Verification of evolving software via component substitutability analysis

Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans Program Lang Syst 17(3):507–534 ABB (2005) http://www.abb.com Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for java classes. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’05), Long Beach, CA, January 12–14, 2005. Assoc Comput Mach, New York, pp 98–109 Alur R, Henzinger T (1996) Reactive modules. In: Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS’96), New Brunswick, NJ, July 27–30, 1996. IEEE Comput Soc Press, Los Alamitos, pp 207–218 Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proc of 17th int conf on computer aided verification Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106 Ball T, Majumdar R, Millstein T, Rajamani S (2001) Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI), Snowbird, UT, June 20–22, 2001. Assoc Comput Mach, New York, pp 203–213 Ball T, Rajamani SK (2000) Boolean programs: a model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research, Redmond, WA, February ftp://ftp.research.microsoft.com/pub/tr/tr-2000-14.pdf Chaki S, Clarke E, Giannakopoulou D, Păsăreanu CS (2004) Abstraction and assume-guarantee reasoning for automated software verification. Technical Report 05.02, Research Institute for Advanced Computer Science (RIACS), Mountain View, CA Chaki S, Sharygina N, Sinha N (2004) Verification of evolving software. In: Proceedings of the third workshop on specification and verification of component based systems (SAVCBS), Newport Beach CA, October 31–November 1, 2004. Iowa State University, Ames, pp 55–61 Chaki S, Clarke E, Groce A, Ouaknine J, Strichman O, Yorav K (2004) Efficient verification of sequential and concurrent C programs. Form Methods Syst Des 25(2–3) Chaki S, Clarke E, Sharygina N, Sinha N (2005) Dynamic component substitutability analysis. In: Proc of conf on formal methods Chaki S, Clarke E, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proc of 17th int conf on computer aided verification Chaki S, Ivers J, Sharygina N, Wallnau K (2005) The comfort reasoning framework. In: Proceedings of the 17th international conference on computer aided verification (CAV’05), Edinburgh Scotland, July 6–10, 2005. Lecture notes in computer science, vol 3576. Springer, New York, pp 164–169 Chaki S, Strichman O (2007) Optimized L * for assume-guarantee reasoning. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS’07) Chakrabarti A, de Alfaro L, Henzinger TA, Jurdzinski M, Mang FYC (2002) Interface compatibility checking for software modules. In: Proceedings of the 14th international conference on computer aided verification (CAV’02), Copenhagen, Denmark, July 27–31, 2002. Lecture notes in computer science, vol 2404. Springer, New York, pp 428–441 Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification (CAV’00), Chicago, IL, July 15–19, 2000. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 154–169 Clarke E, Grumberg O, Long D (1992) Model checking and abstraction. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’92), Albuquerque, NM, January 19–22, 1992. Assoc Comput Mach, New York, pp 343–354 Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons for branching time temporal logic. In: Proceedings of workshop on logic of programs, Yorktown Heights, New York, May 4–6 1982. Lecture notes in computer science, vol 131. Springer, Berlin, pp 52–71 Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Proceedings of the fourth annual IEEE symposium on logic in computer science (LICS’89), Pacific Grove, CA, June 5–8, 1989. IEEE Comput Soc, Los Alamitos, pp 353–362 Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the ninth international conference on tools and algorithms for the construction and analysis of systems (TACAS’03), Warsaw Poland, April 7–11, 2003. Lecture notes in computer science, vol 2619. Springer, New York, pp 331–346 Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: Proc of the ACM/SIGSOFT international symposium on software testing and analysis, pp 97–108 Colón M, Uribe TE (1998) Generating finite-state abstractions of reactive systems using decision procedures. In: Proceedings of the 10th international conference on computer aided verification (CAV’98), Vancouver, Canada, June 28–July 2, 1998. Lecture notes in computer science, vol 1427. Springer, Berlin, pp 293–304 Das S, Dill DL (2001) Successive approximation of abstract transition relations. In: Proceedings of the 16th annual IEEE symposium on logic in computer science (LICS’01), Boston, MA, June 16–19, 2001. IEEE Comput Soc, Los Alamitos, pp 51–60 de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the ninth ACM SIGSOFT symposium on foundations of software engineering (FSE’01), Vienna, Austria, September 10–14, 2001. Assoc Comput Mach, New York, pp 109–120 de Roever WP, Langmaack H, Pnueli A (eds) (1998) Compositionality: the significant difference, international symposium, COMPOS’97, Bad Malente, Germany, September 8–12, 1997. Lecture notes in computer science, vol 1536. Springer, Berlin. (Revised lectures) Dijkstra E (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs Gheorghiu M, Giannakopoulou D, Păsăreanu CS (2007) Refining interface alphabets for compositional verification. In: Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems (TACAS’07) Giannakopoulou D, Păsăreanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of the 17th international conference on automated software engineering (ASE’02), Edinburgh, Scotland, September 23–27, 2002. IEEE Comput Soc, Los Alamitos, pp 3–12 Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: Proceedings of the ninth international conference on computer aided verification (CAV’97), Haifa, Israel, June 22–25, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 72–83 Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS’02), Grenoble, France, April 8–12, 2002. Lecture notes in computer science, vol 2280. Springer, New York, pp 357–370 Gupta A, McMillan K, Fu Z (2007) Automated assumption generation for compositional verification. In: Proceedings of the 19th international conference on computer aided verification (CAV’07) Gurfinkel A, Chechik M (2006) Why waste a perfectly good abstraction? In: Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems, pp 212–226 Gurfinkel A, Wei O, Chechik M (2006) Yasm: A software model-checker for verification and refutation. In: Proc of computer-aided verification, pp 170–174 Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’02). SIGPLAN notices, vol 37(1). Assoc Comput Mach, New York, pp 58–70 Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Reading Ivers J, Sharygina N (2004) Overview of ComForT: a model checking reasoning framework. In: CMU/SEI-2004-TN-018 Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596–619 Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton Liskov BH, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811–1841 MAGIC: http://www.cs.cmu.edu/~chaki/magic McCamant S, Ernst MD (2004) Early identification of incompatibilities in multi-component upgrades. In: Proceedings of the 18th European conference on object-oriented programming (ECOOP’04), Oslo, Norway, June 14–18, 2004. Lecture notes in computer science, vol 3086. Springer, New York, pp 440–464 McMillan K (1997) A compositional rule for hardware design refinement. In: Proceedings of the ninth international conference on computer aided verification (CAV’97), Haifa, Israel, June 22–27, 1997. Lecture notes in computer science, vol 1254. Springer, New York, pp 24–35 Misra J, Chandy KM (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417–426 Nam W, Alur R (2006) Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: 4th International symposium on automated technology for verification and analysis (ATVA’06), pp 170–185 Pnueli A (1985) In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems. Springer, New York, pp 123–144 Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inf Comput 103(2):299–347 Roscoe AW (1998) The theory and practice of concurrency. Prentice-Hall International, New York Shoham S, Grumberg O (2004) Monotonic abstraction-refinement for CTL. In: Proceedings of the 10th international conference on tools and algorithms for the construction and analysis of systems (TACAS’04), pp 546–560 Sinha N, Clarke E (2007) SAT-based compositional verification using lazy learning. In: Proceedings of the 19th international conference on computer aided verification (CAV’07)