Abstract
Model checking is a promising technology for verifying critical behavior of software. However, software model checking is hamstrung by scalability issues and is difficult for software engineers to use directly. The second challenge arises from the gap between model checking concepts and notations, and those used by engineers to develop large-scale systems. ComFoRT [15] addresses both of these challenges. It provides a model checker, Copper, that implements a suite of complementary complexity management techniques to address state space explosion. But ComFoRT is more than a model checker. The ComFoRT reasoning framework includes additional support for building systems in a particular component-based idiom. This addresses transition issues.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Achermann, F., Lumpe, M., Schneider, J., Nierstrasz, O.: Piccola – a Small Composition Language. In: Formal Methods for Distributed Processing–A Survey of Object-Oriented Approaches (2002)
Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (February 2000)
Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. FMSD 25(2) (2004)
Chaki, S., Sharygina, N., Sinha, N.: Verification of evolving software. In: SAVCBS 2004: Worksh. on Specification and Verification of Component-based Systems (2004)
Clarke, E., Chaki, S., Grumberg, O., Touili, T., Ouaknine, J., Sharygina, N., Veith, H.: An expressive verification framework for state/event systems. Technical Report CS-2004-145, CMU (2004)
Clarke, E., Chaki, S., Ouaknine, J., Sharygina, N.: Automated, compositional and iterative deadlock detection. In: 2nd ACM-IEEE MEMOCODE 2004 (2004)
Clarke, E., Chaki, S., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Clarke, E., Chaki, S., Sharygina, N., Sinha, N.: Dynamic component substitutability analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 512–528. Springer, Heidelberg (2005)
Clarke, E., Kroening, 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., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design 25(2) (2004)
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st ICSE (1999)
Hatcliff, J., Deng, X., Dwyer, M.B., Jung, G., Ranganath, V.P.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: ICSE, pp. 160–173 (2003)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages 2002 (2002)
http://www.cs.cmu.edu/chaki/magic Magic tool
Ivers, J., Sharygina, N.: Overview of ComFoRT: A Model Checking Reasoning Framework. Technical Report CMU/SEI-2004-TN-018, SEI, CMU (2004)
Ivers, J., Wallnau, K.: Preserving real concurrency. In: Correctness of model-based software composition Workshop (July 2003)
Wallnau, K.: Vol III: A Technology for Predictable Assembly from Certifiable Components (PACC). Technical Report CMU/SEI-2003-TR-009, SEI,CMU (2003)
Wallnau, K., Ivers, J.: Snapshot of CCL: A Language for Predictable Assembly. Technical Report CMU/SEI-2002-TR-031, SEI, CMU (2002)
Ward-Dutton, N.: Containers: A sign components are growing up. Application Development Trends 46, 41–44 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chaki, S., Ivers, J., Sharygina, N., Wallnau, K. (2005). The ComFoRT Reasoning Framework. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_18
Download citation
DOI: https://doi.org/10.1007/11513988_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)