Abstract
We present FAuST, an extensible framework for Formal verification, Automated debugging, and Software Test generation. Our framework uses a highly customizeable Bounded Model Checking (BMC) algorithm for formal reasoning about software programs and provides different applications, e.g., property checking, functional equivalence checking, test case generation, and fault localization. FAuST supports dynamic execution and parallel symbolic reasoning using the LLVM compiler infrastructure and an abstraction layer for decision procedures.
This work was supported by the German Research Foundation (DFG, grant no. FE 797/6-1).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0 (2010)
Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Symposium on Operating Systems Design and Implementation, pp. 209–224 (2008)
Chipounov, V., Kuznetsov, V., Candea, G.: S2E: A platform for in-vivo multi-path analysis of software systems. In: Conference on Architectural Support for Programming Languages and Operating Systems, pp. 265–278 (2011)
Clarke, E., Kröning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)
de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence 32(1), 97–130 (1987)
Groce, A., Chaki, S., Kröning, D., Strichman, O.: Error explanation with distance metrics. International Journal on Software Tools for Technology Transfer 8(3), 229–247 (2006)
Haedicke, F., Frehse, S., Fey, G., Große, D., Drechsler, R.: metaSMT: Focus on your application not on solver integration. In: International Workshop on Design and Implementation of Formal Tools and Systems, pp. 22–29 (2011)
Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 209–213. Springer, Heidelberg (2008)
Kröning, D.: Software verification. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, pp. 505–532. IOS Press (2009)
Vujošević-Janičić, M., Kuncak, V.: Development and evaluation of LAV: An SMT-based error finding platform. In: International Conference on Verified Software: Theories, Tools and Experiments, pp. 98–113 (2012)
Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization, pp. 75–88 (2004)
Lattner, C., Adve, V.: LLVM language reference manual (2012) (last visit on March 27, 2012)
Li, G., Ghosh, I., Rajan, S.P.: KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 609–615. Springer, Heidelberg (2011)
McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010)
Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In: International Conference on Verified Software: Theories, Tools and Experiments, pp. 146–161 (2012)
Offutt, J., Voas, J.M.: Subsumption of condition coverage techniques by mutation testing. Technical Report ISSE-TR-96-01, George Mason University (1996)
Ramos, D.A., Engler, D.R.: Practical, Low-Effort Equivalence Verification of Real Code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 669–685. Springer, Heidelberg (2011)
Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32(1), 57–95 (1987)
Riener, H., Bloem, R., Fey, G.: Test case generation from mutants using model checking techniques. In: IEEE International Conference on Software Testing, Verification, and Validation Workshops, pp. 388–397 (2011)
Riener, H., Fey, G.: Model-based diagnosis versus error explanation. In: International Conference on Formal Methods and Models for Codesign (to appear, 2012)
Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Symposium on Princples of Programming Languages, pp. 12–27 (1988)
Tseitin, G.S.: On the complexity of derivation in propotional calculus. In: Automation and Reasoning: Classical Papers in Computational Logic 1967-1970 (1983); Originally published in 1970
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Riener, H., Fey, G. (2012). FAuST: A Framework for Formal Verification, Automated Debugging, and Software Test Generation. In: Donaldson, A., Parker, D. (eds) Model Checking Software. SPIN 2012. Lecture Notes in Computer Science, vol 7385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31759-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-31759-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31758-3
Online ISBN: 978-3-642-31759-0
eBook Packages: Computer ScienceComputer Science (R0)