• Consent

  • This survey is part of a study that aims to understand the challenges faced by developers who use Verification-Aware Languages. It seeks to broaden the adoption of these technologies, leading to increased software reliability.

    Purpose

    The purpose of this study is to understand what are the challenges faced by Verification-Aware Language programmers and what can be done to improve those tools to mitigate the discovered challenges.

    Procedures

    In this study, you will answer questions about your knowledge of Verification-Aware Languages. You will need to read an explanation of what we mean by Verification-Aware Languages and answer questions about your experience using Verification-Aware Languages.

    There are groups of questions targeting developers using Dafny and Frama-C. To answer those groups, you will need to read more specific definitions. The expected duration of the survey is from 10 to 15 minutes

    Participant Requirements

    Participation in this study is limited to individuals 18 years of age or older, fluent in English, and with some programming experience with Verification-Aware Languages.

    Risks

    If you agree to participate, the primary risk is a breach of confidentiality since we use a third party (Jotform) to design our survey and collect your data. However, we do not collect any identifiable information. This risk is similar to what you encounter anytime you provide identifiable and private information online. You might encounter boredom or fatigue.

    Usage of Information

    The information collected will be used for scientific publications.

  • I have read and understand the information above.*
  • I want to participate in this research and continue with the survey.*

  • Developer Context

  • Design by Contract is an approach where software designers define formal, precise, and verifiable interface specifications for software components. These specifications extend the type definitions by providing preconditions, post-conditions, and invariants that must be respected across the program.

    Verification-aware languages natively support this approach and come equipped with a program verifier.

    Below is an example of a method to compute the nth term of the Fibonacci sequence using Dafny, a commonly used verification-aware language:

    function fib(n:nat):nat
{
    if n < 2 then n else fib(n-1) + fib(n-2)
}

method ComputeFib(n: nat) returns (f: nat)
    ensures f == fib(n)
{
    f := 0; //fib(0)
    var y := 1; //fib(1)
    var i := 0;
    while i < n
        invariant f == fib(i) && y == fib(i+1) && 0 <= i <= n
    {
            // fib(i) fib(i+1)
        f, y := y, f + y;
        i := i + 1;
    }
}
  • How many years of experience do you have in software development?*
  • How many years of experience do you have with verification-aware languages?*
  • Please select the languages/technologies that you have programming experience with.*
  • Where did you learn about verification-aware languages? Please select all that apply.*
  • Where did you learn how to program with verification-aware languages? Please select all that apply.*

  • Proof Elaboration

  • The following statements regard proof elaboration. Please fill the matrix considering all your knowledge, regardless of the language.*
    Rows

  • Environment Setup

  • Please think about your experience with verification-aware languages, namely the configuration of the development tools. How much do you agree with the following?*
    Rows

  • Feature Knowledge

  • Please recall your knowledge of verification-aware languages and their features and internal mechanisms.*
    Rows

  • Dafny Knowledge

  • The following questions are only about Dafny. Think about your previous experience with Dafny when answering these questions.

  • Please rate your expertise using Dafny on a scale of 0 to 5 with increasing level of skill. Consider your education, experience, publications, and familiarity with techniques and tools.*
  • Are you familiar with Danfy’s memory model? A memory model describes the behavior of accesses to shared variables or heap objects. Its use is usually tied to the keywords “modifies” and “reads”*
  • Please answer these questions based on your knowledge regarding Dafny’s memory model.*
    Rows
  • Are you familiar with the concept of opacity?*
  • How confident are you that you understand what statements are opaque and non-opaque?*
  • Are you familiar with the concept of fuel?*
  • How confident are you that you understand how the fuel attribute works?*
  • Are you familiar with the concept of partial functions?*
  • How confident are you that you can use partial functions to reason about the fulfillment of high-order functions function argument requirements?*
  • Are you familiar with the concept of witnesses?*
  • How confident are you that you can prove the non-emptiness of type definitions by providing witnesses?*

  • Frama-C Knowledge

  • The following questions regard only Frama-C WP Plugin. Please answer, considering your specific experience with this language. For simplicity's sake, we will use Frama-C to refer to the Frama-C WP Plugin from now on.

  • Please rate your expertise using Frama-C with WP Plugin on a scale of 1 to 5 with increasing level of skill. Consider your education, experience, publications, and familiarity with techniques and tools.*
  • Are you familiar with Frama-C WP Plugin memory models? A memory model describes the behavior of accesses to shared variables or heap objects.
  • Please fill out the matrix with your knowledge regarding Frama-C WP Plugin memory model.*
    Rows
  • Please fill in the following matrix regarding your knowledge of Frama-C WP Plugin features.*
    Rows

  • Additional Challenges

  • Overcoming Challenges

  • Overcoming Challenges

  • Rate the importance of the following statements.*
    Rows

  • Demographics

  • How old are you?*
  • How do you describe yourself?*
  • What is the highest level of education you have completed?*
  • Choose one or more races that you consider yourself to be*
  • Are you employed in a computing field (e.g., IT, software engineer, programmer)?*
  • Do you have formal education in a computing field (e.g.,degree in computer science or computer engineering)?*

  • Thank you for your participation

  • Thank you for your participation! Unfortunately, we cannot continue the survey, your participation was filtered out.

  • Should be Empty: