Werner Dietl
Michael D. Ernst
Seth Cooper
ABSTRACT
Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors --- errors that could otherwise disrupt operations in the field. To date, formal verification has been done by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.
Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task --- a game --- that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.
This paper presents a status report on the Verification Games project and our Pipe Jam prototype game.
- A. Aiken, S. Bugrara, I. Dillig, T. Dillig, P. Hawkins, and B. Hackett. An overview of the Saturn project. In PASTE, pages 43--48, 2007. Google Scholar
Digital Library
- T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: static driver verification with under 4% false alarms. In FMCAD, pages 35--42, 2010. Google ScholarDigital Library
- T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. CACM, 54:68--76, July 2011. Google ScholarDigital Library
- T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI, pages 203--213, June 2001. Google ScholarDigital Library
- Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions. Springer-Verlag, 2004. Google ScholarDigital Library
- A. Birka and M. D. Ernst. A practical type system and language for reference immutability. In OOPSLA, pages 35--49, Oct. 2004. Google ScholarDigital Library
- G. Bracha. Pluggable type systems. In RDL, Oct. 2004.Google Scholar
- Checker Framework website. http://types.cs.washington.edu/checker-framework/.Google Scholar
- S. Cooper. A Framework for Scientific Discovery through Video Games. PhD thesis, University of Washington, Seattle, WA, 2011.Google Scholar
- S. Cooper, F. Khatib, I. Makedon, H. Lu, J. Barbero, J. Fogarty, Z. Popović, and Foldit Players. Analysis of social gameplay macros in the Foldit cookbook. In FDG, 2011. Google ScholarDigital Library
- S. Cooper, F. Khatib, A. Treuille, J. Barbero, J. Lee, M. Beenen, A. Leaver-Fay, D. Baker, Z. Popović, and Foldit Players. Predicting protein structures with a multiplayer online game. Nature, 466(7307):756--760, 2010.Google ScholarCross Ref
- S. Cooper, A. Treuille, J. Barbero, A. Leaver-Fay, K. Tuite, F. Khatib, A. C. Snyder, M. Beenen, D. Salesin, D. Baker, Z. Popović, and Foldit Players. The challenge of designing scientific discovery games. In FDG, 2010. Google ScholarDigital Library
- T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95--120, Feb. 1988. Google ScholarDigital Library
- P. Cousot. Types as abstract interpretations. In POPL, pages 316--331, 1997. Google ScholarDigital Library
- P. Cousot. The verification grand challenge and abstract interpretation. In Verified Software: Theories, Tools, Experiments, pages 227--240. Dec. 2007.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Temporal abstract interpretation. In POPL, pages 12--25, 2000. Google ScholarDigital Library
- W. Dietl. Universe Types: Topology, Encapsulation, Genericity, and Tools. PhD thesis, Department of Computer Science, ETH Zurich, Dec. 2009. Doctoral Thesis ETH No. 18522.Google Scholar
- W. Dietl, S. Dietzel, M. D. Ernst, K. Muşlu, and T. Schiller. Building and using pluggable type-checkers. In ICSE, pages 681--690, May 2011. Google ScholarDigital Library
- W. M. Dietl, M. D. Ernst, and P. Müller. Tunable static inference for Generic Universe Types. In ECOOP, pages 333--357, July 2011. Google ScholarDigital Library
- M. D. Ernst. Static and dynamic analysis: Synergy and duality. In WODA, pages 24--27, May 2003.Google Scholar
- D. Greenfieldboyce and J. S. Foster. Type qualifiers for Java. http://www.cs.umd.edu/Grad/scholarlypapers/papers/greenfiledboyce.pdf, Aug. 8, 2005.Google Scholar
- D. Greenfieldboyce and J. S. Foster. Type qualifier inference for Java. In OOPSLA, pages 321--336, Oct. 2007. Google ScholarDigital Library
- Web interface to the Julia analyzer. http://julia.scienze.univr.it.Google Scholar
- G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an operating system kernel. CACM, 53(6):107--115, June 2010. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. CACM, 52(7), July 2009. Google ScholarDigital Library
- P. Martin-Löf. Intuitionistic type theory: notes by Giovanni Sambin of a series of lectures given in Padua. Studies in proof theory/Lecture notes, 1. Bibliopolis, 1984.Google Scholar
- M. Naik and J. Palsberg. A type system equivalent to a model checker. In ESOP, pages 374--388. 2005. Google ScholarDigital Library
- T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. 2002. Google ScholarDigital Library
- M. M. Papi, M. Ali, T. L. Correa Jr., J. H. Perkins, and M. D. Ernst. Practical pluggable types for Java. In ISSTA, pages 201--212, July 2008. Google ScholarDigital Library
- J. Quinonez. Inference of reference immutability in Java. Master's thesis, MIT Dept. of EECS, May 2008.Google Scholar
- J. Quinonez, M. S. Tschantz, and M. D. Ernst. Inference of reference immutability. In ECOOP, pages 616--641, July 2008. Google ScholarDigital Library
- M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. 2006. Google ScholarDigital Library
- F. Spoto. Nullness analysis in boolean form. In SEFM, Nov. 2008. Google ScholarDigital Library
- F. Spoto. The nullness analyser of Julia. In LPAR, Apr. 2010. Google ScholarDigital Library
- F. Spoto. Precise null-pointer analysis. Software and Systems Modeling, 2010. Google ScholarDigital Library
- F. Spoto and M. D. Ernst. Inference of field initialization. In ICSE, pages 231--240, May 2011. Google ScholarDigital Library
- M. S. Tschantz. Javari: Adding reference immutability to Java. Master's thesis, MIT Dept. of EECS, Aug. 2006.Google Scholar
- M. S. Tschantz and M. D. Ernst. Javari: Adding reference immutability to Java. In OOPSLA, pages 211--230, Oct. 2005. Google ScholarDigital Library
Index Terms
- Verification games: making verification fun
Recommendations
Types and higher-order recursion schemes for verification of higher-order programs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
Efficient and User-Friendly Verification
A compositional verification method from a high-level resource-management standpoint is presented for dense-time concurrent systems and implemented in the tool of SGM (State-Graph Manipulators) with graphical user interface. SGM packages sophisticated ...
Formal semantics, modular specification, and symbolic verification of product-line behaviour
Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated ...
Comments