Willem Visser
Nikolaj Bjørner
ABSTRACT
Software poses a range of engineering challenges. How do we capture the expected behavior of the software? How can we check if such behavioral descriptions are consistent and valid? How do we generate test instances that explore and examine different parts of the software. We focus on the underlying technology by which a number of these problems can be reduced to a logical form and answered using automated deduction. In the first part we briefly summarize the use of automated deduction within software engineering. Then we consider some of the current and future trends in software engineering and the type of advances it may require from automated deduction. We observe that in the past software engineering problems were solved by merely leveraging advances in automated deduction, especially in SAT and SMT solving, whereas we are now entering a phase where advances in automated deduction are also driven by software engineering requirements.
- G. Audemard and L. Simon. Predicting Learnt Clauses Quality in Modern SAT Solvers. In C. Boutilier, editor, IJCAI, pages 399–404, 2009. Google Scholar
Digital Library
- T. Ball, E. Bounimova, V. Levin, R. Kumar, and J. Lichtenberg. The static driver verifier research platform. In Proceedings of the 22Nd International Conference on Computer Aided Verification, CAV’10, pages 119–122, Berlin, Heidelberg, 2010. Springer. Google ScholarDigital Library
- T. Ball, B. Hackett, S. K. Lahiri, S. Qadeer, and J. Vanegue. Towards scalable modular checking of user-defined properties. In G. T. Leavens, P. W. O’Hearn, and S. K. Rajamani, editors, VSTTE, volume 6217 of LNCS, pages 1–24. Springer, 2010. Google ScholarDigital Library
- J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003. Google ScholarDigital Library
- M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and verification: the Spec# experience. Commun. ACM, 54(6):81–91, 2011. Google ScholarDigital Library
- C. Barrett and C. Tinelli. CVC3. In W. Damm and H. Hermanns, editors, CAV, volume 4590 of LNCS, pages 298–302. Springer, 2007. Google ScholarDigital Library
- B. Beckert, R. Hähnle, and P. H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer, 2007. Google ScholarDigital Library
- Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Springer, 2004. Coq home page: http://coq.inria.fr/. Google ScholarDigital Library
- W. R. Bevier, W. A. Hunt, Jr., J. S. Moore, and W. D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, Dec. 1989. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The Software Model Checker Blast: Applications to Software Engineering. Int. J. Softw. Tools Technol. Transf., 9(5):505–525, Oct. 2007. Google ScholarDigital Library
- A. Biere. Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In Proceedings of SAT Competition 2013, volume B-2013-1 of Department of Computer Science Series of Publications B, pages 51–52, 2013.Google Scholar
- A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google ScholarDigital Library
- M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodríguez-Carbonell, and A. Rubio. The Barcelogic SMT solver. In A. Gupta and S. Malik, editors, Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of LNCS, pages 294–298. Springer, 2008. Google ScholarDigital Library
- E. Bounimova, P. Godefroid, and D. Molnar. Billions and billions of constraints: Whitebox fuzz testing in production. In Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, pages 122–131, Piscataway, NJ, USA, 2013. IEEE Press. Google ScholarDigital Library
- R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT—A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 10(6):234–245, June 1975. Google ScholarDigital Library
- R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, NY, 1988. Google ScholarDigital Library
- R. Brummayer and A. Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, pages 174–177. Springer, 2009. Google ScholarDigital Library
- R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, and R. Sebastiani. The MathSAT 4 SMT solver. In A. Gupta and S. Malik, editors, Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of LNCS, pages 299–303. Springer, 2008. Google ScholarDigital Library
- R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986. Google ScholarDigital Library
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10 20 states and beyond. Information and Computation, 98(2):142–170, June 1992. Google ScholarDigital Library
- M. Buro and H. K. Büning. Report on a SAT Competition. Bulletin of the EATCS, 49, 1993.Google Scholar
- W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Softw., Pract. Exper., 30(7):775–802, 2000. Google ScholarDigital Library
- R. Butler, G. Hagen, J. Maddalon, C. Muñoz, A. Narkawicz, and G. Dowek. How formal methods impels discovery: A short history of an air traffic management project. In C. Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pages 34–46, Langley Research Center, Hampton VA, USA, April 2010. NASA.Google Scholar
- C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209–224. USENIX Association, 2008. Google ScholarDigital Library
- C. Cadar, P. Godefroid, S. Khurshid, C. S. Pasareanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: preliminary assessment. In R. N. Taylor, H. Gall, and N. Medvidovic, editors, ICSE, pages 1066–1071. ACM, 2011. Google ScholarDigital Library
- P. Chalin, J. R. Kiniry, G. T. Leavens, and E. Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, editors, FMCO, volume 4111 of LNCS, pages 342–363. Springer, 2005. Google ScholarDigital Library
- C.-H. Cheng, N. Shankar, H. Ruess, and S. Bensalem. EFSMT: A logical framework for cyber-physical systems. arXiv preprint arXiv:1306.3456, 2013.Google Scholar
- A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In E. Brinksma and K. Larsen, editors, Computer Aided Verification, volume 2404 of LNCS, pages 359–364. Springer, 2002. Google ScholarDigital Library
- E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Form. Methods Syst. Des., 19(1):7–34, July 2001. Google ScholarDigital Library
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, Sept. 2003. Google ScholarDigital Library
- L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, 2(3):215–222, Sept. 1976. Google ScholarDigital Library
- E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In Theorem Proving in Higher Order Logics, pages 23–42. Springer, 2009. Google ScholarDigital Library
- R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ, 1986. Nuprl home page: http://www.cs. cornell.edu/Info/Projects/NuPRL/. Google ScholarDigital Library
- B. Cook, J. Fisher, E. Krepska, and N. Piterman. Proving stabilization of biological systems. In R. Jhala and D. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation, volume 6538 of LNCS, pages 134–149. Springer, 2011. Google ScholarDigital Library
- S. Cruanes, G. Hamon, S. Owre, and N. Shankar. Tool Integration with the Evidential Tool Bus. In VMCAI, pages 275–294, 2013.Google ScholarDigital Library
- P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C a software analysis perspective. In G. Eleftherakis, M. Hinchey, and M. Holcombe, editors, SEFM, volume 7504 of LNCS, pages 233–247. Springer, 2012. Google ScholarDigital Library
- M. Davis, G. Logemann, and D. W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394–397, 1962. Google ScholarDigital Library
- M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201–215, 1960. Google ScholarDigital Library
- L. de Moura, S. Owre, H. Rueß, J. Rushby, N. Shankar, M. Sorea, and A. Tiwari. SAL 2. In R. Alur and D. Peled, editors, Computer Aided Verification, volume 3114 of LNCS, pages 496–500. Springer, 2004.Google ScholarCross Ref
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, volume 4963 of LNCS, pages 337–340. Springer, 2008. Google ScholarDigital Library
- D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365–473, 2005. Google ScholarDigital Library
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report 159, COMPAQ Systems Research Center, 1998.Google Scholar
- B. Dutertre and L. de Moura. A fast linear-arithmetic solver for DPLL(T). In T. Ball and R. B. Jones, editors, CAV, volume 4144 of LNCS, pages 81–94. Springer, 2006. Google ScholarDigital Library
- N. Eén and N. Sörensson. An Extensible SAT-solver. In E. Giunchiglia and A. Tacchella, editors, SAT, volume 2919 of LNCS, pages 502–518. Springer, 2003.Google Scholar
- B. Elspas, K. N. Levitt, R. J. Waldinger, and A. Waksman. An assessment of techniques for proving program correctness. ACM Comput. Surv., 4(2):97–147, 1972. Google ScholarDigital Library
- A. Filieri, C. S. Păsăreanu, and W. Visser. Reliability analysis in Symbolic Pathfinder. In Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, pages 622–631, Piscataway, NJ, USA, 2013. IEEE Press. Google ScholarDigital Library
- J. Fisher, D. Harel, and T. A. Henzinger. Biology as reactivity. Commun. ACM, 54(10):72–82, Oct. 2011. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. In J. Knoop and L. J. Hendren, editors, PLDI, pages 234–245. ACM, 2002. Google ScholarDigital Library
- R. W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, volume XIX, pages 19–32. American Mathematical Society, Providence, Rhode Island, 1967.Google Scholar
- V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In W. Damm and H. Hermanns, editors, CAV, volume 4590 of LNCS, pages 519–531. Springer, 2007. Google ScholarDigital Library
- J. Geldenhuys, M. B. Dwyer, and W. Visser. Probabilistic symbolic execution. In Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, pages 166–176, New York, USA, 2012. ACM. Google ScholarDigital Library
- C. P. Gomes, B. Selman, and H. A. Kautz. Boosting combinatorial search through randomization. In J. Mostow and C. Rich, editors, AAAI/IAAI, pages 431–437. AAAI Press / The MIT Press, 1998. Google ScholarDigital Library
- G. Gonthier. Formal proof: The four-color theorem. Notices of the AMS, 55(11):1382–1394, Dec. 2008.Google Scholar
- M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993. HOL home page: http: //www.cl.cam.ac.uk/Research/HVG/HOL/. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 62–73, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- F. Haedicke, S. Frehse, G. Fey, D. Grosse, and R. Drechsler. metaSMT: Focus On Your Application Not On Solver Integration. In Proceedings of the First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), 2011.Google Scholar
- J. Y. Halpern, R. Harper, N. Immerman, P. G. Kolaitis, M. Vardi, and V. Vianu. On the unusual effectiveness of logic in computer science. The Bulletin of Symbolic Logic, 7(2):213–236, 2001.Google ScholarCross Ref
- C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576–583, 1969. Google ScholarDigital Library
- G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. Google ScholarDigital Library
- F. Howar, M. Isberner, M. Merten, B. Steffen, and D. Beyer. The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. In T. Margaria and B. Steffen, editors, ISoLA (1), volume 7609 of LNCS, pages 608–614. Springer, 2012. Google ScholarDigital Library
- D. Jackson. Alloy: A new technology for software modelling. In J.-P. Katoen and P. Stevens, editors, TACAS, volume 2280 of LNCS, page 20. Springer, 2002. Google ScholarDigital Library
- E. K. Jackson and W. Schulte. Formula 2.0: A language for formal specifications. In Z. Liu, J. Woodcock, and H. Zhu, editors, ICTAC Training School on Software Engineering, volume 8050 of LNCS, pages 156–206. Springer, 2013.Google Scholar
- M. Jose and R. Majumdar. Cause clue clauses: Error localization using maximum satisfiability. SIGPLAN Not., 46(6):437–446, June 2011. Google ScholarDigital Library
- M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach, volume 3 of Advances in Formal Methods. Kluwer, 2000. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. CACM, 19(7):385–394, 1976. Google ScholarDigital Library
- 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. Commun. ACM, 53(6):107–115, 2010. Google ScholarDigital Library
- L. Kovács and A. Voronkov. First-Order Theorem Proving and Vampire. In Sharygina and Veith {102}, pages 1–35.Google Scholar
- M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. SIGMETRICS Perform. Eval. Rev., 36(4):40–45, Mar. 2009. Google ScholarDigital Library
- A. Legay, B. Delahaye, and S. Bensalem. Statistical model checking: An overview. In H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund, I. Lee, G. Pace, G. Rosu, O. Sokolsky, and N. Tillmann, editors, Runtime Verification, volume 6418 of LNCS, pages 122–135. Springer, 2010. Google ScholarDigital Library
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370. Springer, 2010. Google ScholarDigital Library
- K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In K. Koskimies, editor, CC, volume 1383 of LNCS, pages 302–305. Springer, 1998. Google ScholarDigital Library
- K. R. M. Leino and P. Rümmer. A polymorphic intermediate verification language: Design and logical encoding. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’10, pages 312–327, Berlin, Heidelberg, 2010. Springer. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107–115, 2009. Google ScholarDigital Library
- D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal Verifier user manual. CSD Report STAN-CS-79-731, Stanford University, Stanford, CA, Mar. 1979. Google Scholar
- P. Madhusudan and X. Qiu. Efficient Decision Procedures for Heaps Using STRAND. In E. Yahav, editor, SAS, volume 6887 of LNCS, pages 43–59. Springer, 2011. Google ScholarDigital Library
- J. P. Marques-Silva and K. A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. In ICCAD, 1996.Google ScholarCross Ref
- J. McCarthy. Recursive functions of symbolic expressions and their computation by machine. Commun. ACM, 3(4):184–195, 1960. Google ScholarDigital Library
- S. McPeak, C.-H. Gros, and M. K. Ramanathan. Scalable and incremental software bug detection. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pages 554–564, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- F. L. Morris and C. B. Jones. An Early Program Proof by Alan Turing. Annals of the History of Computing, 6:139–143, 1984. Google ScholarDigital Library
- C. A. Muñoz, V. Carreño, G. Dowek, and R. W. Butler. Formal verification of conflict detection algorithms. STTT, 4(3):371–380, 2003.Google ScholarCross Ref
- G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.Google Scholar
- J. v. Neumann and H. H. Goldstine. Planning and coding of problems for an electronic computing instrument. Institute for Advanced Study, Princeton, New Jersey, 1948. Reprinted in {113}.Google Scholar
- H. D. T. Nguyen, D. Qi, A. Roychoudhury, and S. Chandra. Semfix: program repair via semantic analysis. In D. Notkin, B. H. C. Cheng, and K. Pohl, editors, ICSE, pages 772–781. IEEE / ACM, 2013. Google ScholarDigital Library
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. Isabelle home page: http://isabelle.in.tum.de/. Google ScholarCross Ref
- P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In L. Fribourg, editor, CSL, volume 2142 of LNCS, pages 1–19. Springer, 2001. Google ScholarDigital Library
- S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEETSE, 21(2):107–125, Feb. 1995. PVS home page: http://pvs.csl.sri.com. Google ScholarDigital Library
- H. Palikareva and C. Cadar. Multi-solver support in symbolic execution. In Sharygina and Veith {102}, pages 53–68. Google ScholarDigital Library
- F. Pelletier, G. Sutcliffe, and C. Suttner. The Development of CASC. AI Communications, 15(2-3):79–90, 2002. Google ScholarDigital Library
- C. S. Pˇasˇareanu, W. Visser, D. Bushnell, J. Geldenhuys, P. Mehlitz, and N. Rungta. Symbolic PathFinder: Integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, 20(3):391–425, 2013.Google ScholarCross Ref
- S. Rajan, N. Shankar, and M. Srivas. An integration of model-checking with automated proof checking. In P. Wolper, editor, CAV, volume 939 of LNCS, pages 84–97, Liege, Belgium, June 1995. Springer Verlag. Google ScholarDigital Library
- A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001. Google ScholarDigital Library
- J. A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965. Reprinted in Siekmann and Wrightson {103}, pages 397–415. Google ScholarDigital Library
- J. Rushby, F. von Henke, and S. Owre. An introduction to formal specification and verification using E HDM. Technical Report SRI-CSL-91-2, CSL, MP, Feb. 1991.Google Scholar
- J. M. Rushby. An evidential tool bus. In K.-K. Lau and R. Banach, editors, ICFEM, volume 3785 of LNCS, pages 36–36. Springer, 2005. Google ScholarDigital Library
- S. Sankaranarayanan, A. Chakarov, and S. Gulwani. Static analysis for probabilistic programs: Inferring whole program properties from finitely many paths. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, pages 447–458, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- P. H. Schmitt, M. Ulbrich, and B. Weiß. Dynamic frames in Java dynamic logic. In B. Beckert and C. Marché, editors, Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of LNCS, pages 138–152. Springer, 2011. Google ScholarDigital Library
- S. Schulz. System Description: E 1.8. In K. McMillan, A. Middeldorp, and A. Voronkov, editors, Proc. of the 19th LPAR, Stellenbosch, volume 8312 of LNCS. Springer, 2013.Google ScholarCross Ref
- N. Shankar. Metamathematics, Machines, and Gödel’s Proof. Cambridge Tracts in Theoretical Computer Science. CUP, Cambridge, UK, 1994. Google ScholarDigital Library
- N. Shankar. Using decision procedures with a higher-order logic. In Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of LNCS, pages 5–26, Edinburgh, Scotland, Sept. 2001. Springer Verlag. Google ScholarDigital Library
- N. Shankar. Trust and automation in verification tools. In S. S. Cha, J.-Y. Choi, M. Kim, I. Lee, and M. Viswanathan, editors, 6th International Symposium on Automated Technology for Verification and Analysis (ATVA 2008), volume 5311 of LNCS, pages 4–17. Springer Verlag, Oct. 2008. Google ScholarDigital Library
- N. Shankar. Automated deduction for verification. ACM Comput. Surv, 41(4):20:1–56, 2009. Google ScholarDigital Library
- N. Sharygina and H. Veith, editors. Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of LNCS. Springer, 2013.Google ScholarCross Ref
- J. Siekmann and G. Wrightson, editors. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer, 1983.Google Scholar
- R. Singh, S. Gulwani, and A. Solar-Lezama. Automated feedback generation for introductory programming assignments. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, pages 15–26, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XII, pages 404–415, New York, NY, USA, 2006. ACM. Google ScholarDigital Library
- K. T. Stolee and S. Elbaum. Toward Semantic Search via SMT Solver. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, FSE ’12, pages 25:1–25:4, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009. Google ScholarDigital Library
- G. Sutcliffe. The 6th IJCAR Automated Theorem Proving System Competition - CASC-J6. AI Communications, 26(2):211–223, 2013. Google ScholarDigital Library
- G. Sutcliffe and C. Suttner. The State of CASC. AI Communications, 19(1):35–48, 2006. Google ScholarDigital Library
- W. Visser, J. Geldenhuys, and M. B. Dwyer. Green: Reducing, Reusing and Recycling Constraints in Program Analysis. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, FSE ’12, pages 58:1–58:11, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engg., 10(2):203–232, Apr. 2003. Google ScholarDigital Library
- W. Visser, C. S. Pˇasˇareanu, and S. Khurshid. Test input generation with Java PathFinder. In Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA ’04, pages 97–107, New York, NY, USA, 2004. ACM. Google ScholarDigital Library
- J. von Neumann. John von Neumann, Collected Works, Volume V. Pergamon Press, Oxford, 1961.Google Scholar
- C. Weidenbach, U. Brahm, T. Hillenbrand, E. Keen, C. Theobalt, and D. Topic. SPASS version 2.0. In A. Voronkov, editor, Automated Deduction – CADE-18, volume 2392 of LNCS, pages 275–279. Springer, July 27-30 2002. Google ScholarDigital Library
Index Terms
- Software engineering and automated deduction
Recommendations
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
AbstractWe discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with ...
Automated Deduction Techniques for Studying Rough Algebras
We present a non-exhaustive state of the art in the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting deduction steps, for eliminating redundant information, for ...
Informational logic in knowledge representation and automated deduction
Informational logic is a new approach to the formalization of the notion of rational conjecture that is of interest both from the epistemic and the automated reasoning point of view. Given a logical system $T$, an informational logic is based on a new ...
Comments