Reducing the barriers to writing verified specifications

ABSTRACT

Formally verifying a program requires significant skill not only because of complex interactions between program subcomponents, but also because of deficiencies in current verification interfaces. These skill barriers make verification economically unattractive by preventing the use of less-skilled (less-expensive) workers and distributed workflows (i.e., crowdsourcing). This paper presents VeriWeb, a web-based IDE for verification that decomposes the task of writing verifiable specifications into manageable subproblems. To overcome the information loss caused by task decomposition, and to reduce the skill required to verify a program, VeriWeb incorporates several innovative user interface features: drag and drop condition construction, concrete counterexamples, and specification inlining.

To evaluate VeriWeb, we performed three experiments. First, we show that VeriWeb lowers the time and monetary cost of verification by performing a comparative study of VeriWeb and a traditional tool using 14 paid subjects contracted hourly from Exhedra Solution's vWorker online marketplace. Second, we demonstrate the dearth and insufficiency of current ad-hoc labor marketplaces for verification by recruiting workers from Amazon's Mechanical Turk to perform verification with VeriWeb. Finally, we characterize the minimal communication overhead incurred when VeriWeb is used collaboratively by observing two pairs of developers each use the tool simultaneously to verify a single program.

References

1. Amazon Mechanical Turk, Apr. 2012. https://www.mturk.com/.
2. M. Barnett, B.-Y. E. Chang, R. DeLine, B. J. 002, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, pages 364--387, 2005.
3. M. Barnett, M. Fahndrich, P. de Halleux, F. Logozzo, and N. Tillmann. Exploiting the synergy between automated-test-generation and programming-by-contract. In 31st International Conference on Software Engineering, pages 401--402, May 2009.
4. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec\# programming system: An overview. In CASSIS, pages 49--69, Mar. 2004.
5. M. S. Bernstein, G. Little, R. C. Miller, B. Hartmann, M. S. Ackerman, D. R. Karger, D. Crowell, and K. Panovich. Soylent: a word processor with a crowd inside. In Proceedings of the 23nd annual ACM symposium on User interface software and technology, UIST '10, pages 313--322, New York, NY, USA, 2010. ACM.
6. L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7(3):212--232, June 2005.
7. B. V. Chess. Improving computer security using Extended Static Checking. In IEEE Symposium on Security and Privacy, pages 160--173, Berkeley, California, May 12--15, 2002.
8. Code Contracts user manual. http://download.microsoft.com/download/C/2/7/C2715F76-F56C-4D37--9231-EF%8076B7EC13/userdoc.pdf, Sept. 2010.
9. D. R. Cok and J. R. Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2004, Revised Selected Papers, volume 3362 of LNCS, pages 108--128, Marseille, France, Mar. 10--13, 2004.
10. P. Dai, Mausam, and D. S. Weld. Decision-theoretic control of crowd-sourced workflows. In AAAI Conference on Artificial Intelligence, pages 1168--1174, 2010.
11. L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, Apr. 2008.
12. D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003--148, HP Labs, Palo Alto, CA, July 23, 2003.
13. D. L. Detlefs. An overview of the Extended Static Checking system. In Proceedings of the First Workshop on Formal Methods in Software Practice, pages 1--9, Jan. 1996.
14. D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, Dec. 18, 1998.
15. 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.
16. M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):99--123, Feb. 2001.
17. M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Programming, 69(1--3):35--45, Dec. 2007.
18. C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In Formal Methods Europe, pages 500--517, Mar. 2001.
19. C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, pages 234--245, June 2002.
20. J. J. Horton and L. B. Chilton. The labor economics of paid crowdsourcing. In Proceedings of the 11th ACM Conference on Electronic Commerce, EC '10, pages 209--218, 2010.
21. J. R. Kiniry, A. E. Morkan, and B. Denby. Soundness and completeness warnings in ESC/Java2. In Proceedings of the Fifth International Workshop on Specification and Verification of Component Based Systems (SAVCBS), 2006.
22. G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM Softw. Eng. Notes, 31(3), Mar. 2006.
23. K. Leino. Dafny: An automatic program verifier for functional correctness. In E. Clarke and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 6355 of Lecture Notes in Computer Science, pages 348--370. Springer Berlin / Heidelberg, 2010.
24. K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In Compiler Construction '98, pages 302--305, Apr. 1998.
25. G. Little, L. B. Chilton, M. Goldman, and R. C. Miller. Turkit: tools for iterative tasks on mechanical turk. In Proceedings of the ACM SIGKDD Workshop on Human Computation, HCOMP '09. ACM, 2009.
26. W. Mason and D. J. Watts. Financial incentives and the "performance of crowds". In Proceedings of the ACM SIGKDD Workshop on Human Computation, HCOMP '09, pages 77--85, New York, NY, USA, 2009. ACM.
27. G. Nelson. Techniques for Program Verification. PhD thesis, Stanford University, Palo Alto, CA, 1980. Also published as Xerox Palo Alto Research Center Research Report CSL-81--10.
28. J. W. Nimmer and M. D. Ernst. Invariant inference for static checking: An empirical evaluation. In FSE, pages 11--20, Nov. 2002.
29. 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.
30. Purchasing power parities for GDP and related indicators. http://stats.oecd.org/Index.aspx?DataSetCode=PPPGDP, Apr. 2012.
31. T. W. Schiller and M. D. Ernst. Rethinking the economics of software engineering. In FoSER, pages 325--330, Nov. 2010.
32. T. Sheard, A. Stump, and S. Weirich. Language-based verification will change the world. In Proceedings of the FSE/SDP workshop on Future of software engineering research, FoSER '10, pages 343--348, New York, NY, USA, 2010. ACM.
33. K. T. Stolee and S. Elbaum. Exploring the use of crowdsourcing to support empirical studies in software engineering. In Proceedings of the 2010 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, ESEM '10, pages 35:1--35:4, New York, NY, USA, 2010. ACM.
34. N. Tillmann, J. de Halleux, and T. Xie. Pex for fun: Engineering an automated testing tool for serious games in computer science. Technical Report MSR-TR-2011--41, Microsoft Research, Redmond, WA, March 2011.
35. U.S. Bureau of Labor Statistics. Computer software engineers, applications, May 2010. http://www.bls.gov/oes/current/oes151031.htm.
36. uTest: Software testing, Apr. 2012. http://www.utest.com.
37. vWorker.com: More capable, accountable and affordable. guaranteed., Apr. 2012. http://www.vworker.com.
38. Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer. Inferring better contracts. In Proceedings of 2011 International Conference on Software Engineering (ICSE 2011), 2011.
39. M. A. Weiss. Data Structures and Algorithm Analysis in Java. Addison Wesley Longman, 1999.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification