Abstract
Theorem proving and model checking are two well-known formal methods emerging recently for software verification. Each of them has its own advantages and disadvantages. As an attempt to combine the verification capabilities of these two methods, in this paper we introduce a verification tool known as COMBINE (Combined fOrmal Methods for BINdingly vErification). Suggested by its name, COMBINE can verify imperative programs in a bindingly manner comprising of two phases: static verification and dynamic verification. In fact, COMBINE has been developed as a published Web-based system currently being used for teaching programming for students at Hochiminh City University of Technology (HCMUT), Vietnam.
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.
References
Clarke, E.M., Wing, J.M., et al.: Formal methods: State of the art and future directions. ACM Survey 28, 626–643 (1996)
Duffy, D.A.: Principles of Automated Theorem Proving. John Wiley & Sons, Chichester (1991)
Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Conference Record for of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 191–202 (2002)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs, 52–71 (1981)
Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, preliminary design (version 1.4) (October 2008)
Necula, G.C., Mcpeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: International Conference on Compiler Construction, pp. 213–228 (2002)
Quan, T.T., Hoang, D.L.N., Nguyen, B.T., Nguyen, A.N., Tran, Q.D., Nguyen, P.H., Bui, T.H., et al.: MAFSE: A model-based framework for software verification. In: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement, Singapore (2010)
Quan, T.T., Hoang, D.L.N., Nguyen, V.H., Nguyen, P.H.: Model–based Generation of Structured Error–Flows in Imperative Programs. In: Proceedings of International Conference on Advanced Computing and Applications (ACOMP 2010), Vietnam (2010)
Z3: An Efficient SMT Solver, http://research.microsoft.com/en-us/um/redmond/projects/z3/
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking, Tehcnical report, http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html
The Alt-Ergo Theorem Prover, http://alt-ergo.lri.fr/
Frama-C, http://frama-c.com/
Jessie plugin, http://frama-c.cea.fr/jessie.html
Spin – Formal Verification, http://spinroot.com/
The Coq Proof Assistant, http://www.lix.polytechnique.fr/coq/
Redlog, http://redlog.dolzmann.de/
Why: a software verification platform, http://why.lri.fr/
HIP Overview, http://loris-7.ddns.comp.nus.edu.sg/~project/hip/index.html.
Java PathFinder, http://babelfish.arc.nasa.gov/trac/jpf
NuSMV – a new symbolic model checker, http://nusmv.fbk.eu/
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002: Principles of Programming Languages, pp. 58–70 (2002)
Flanagan, C.: Hybrid type checking. In: POPL 2006: Principles of Programming Languages, pp. 245–256 (2006)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, pp. 268–279 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, A.N., Quan, T.T., Nguyen, P.H., Bui, T.H. (2010). COMBINE: A Tool on Combined Formal Methods for Bindingly Verification. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)