Software Verification-Silicon Valley Campus - Carnegie Mellon University

Software Verification

image of code

Our research in software verification investigates the use of abstraction and symbolic execution techniques in the context of the open source Java PathFinder verification tool set, with applications to test input generation and error detection. Towards this end, we are developing Symbolic PathFinder, a symbolic execution tool for Java bytecode. The tool is used in various projects at NASA and in industry (most notably at Fujitsu Labs) and also in academia. We are also working on using learning techniques for automating assume-guarantee style compositional verification. recently, we have investigated compositional techniques for scaling the analysis of probabilistic systems. Furthermore, we are working on parallelization of verification tasks and on modeling and analysis for multiple statechart formalisms.

A second research thrust focuses on algorithms and techniques for specializing static analyzers in order to achieve high precision and performance on large codes. We have developed a static analysis engine named IKOS (Inference Kernel of Open Static Analyzers), which implements advanced static analysis algorithms beneath a highly generic API. Specializing a static analyzer for a certain application or family of applications is key to achieving the high precision required to use the technology in a certification process. IKOS streamlines the development of specialized static analyzers by encapsulating the complex algorithmics involved and letting the developer focus on the specificities of the application considered. IKOS has been used to design static analyzers for flight software that perform the formal verification of critical properties of the application (like the absence of buffer overflows) and yield a low rate of false positives.IKOS is slated for open-source release under the NASA Open Source Agreement (NOSA). Ongoing research focuses on designing new static analysis algorithms to improve the precision and scalability of the tool.

Faculty

Guillame Brat, Corina Pasareanu, Arnaud Venet

Papers

  • Misty Davies, Corina S. Pasareanu, Vishwanath Raman : Symbolic Execution Enhanced System Testing. VSTTE 2012 : 294-309 (2012)
  • Perry Alexander, Corina S. Pasareanu, John G. Hosking : 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA, November 6-10,  (2011)
  • Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Pasareanu, Koushik Sen, Nikolai Tillmann, Willem Visser : Symbolic Execution for Software Testing in Practice – Preliminary Assessment. ICSE 2011 : 1066-1071 (2011)
  • Domenico Bianculli, Dimitra Giannakopoulou, Corina S. Pasareanu: Interface decomposition for service compositions. ICSE 2011 : 501-510  (2011)
  • Corina S. Pasareanu, Neha Rungta, Willem Visser : Symbolic execution with mixed concrete-symbolic solving. ISSTA 2011 : 34-44  (2011)
  • Daniel Balasubramanian, Corina S. Pasareanu, Michael W. Whalen, Gabor Karsai, Michael R. Lowry : Polyglot: modeling and analysis for multiple Statechart formalisms. ISSTA 2011 : 45-55  (2011)
  • Daniel Balasubramanian, Gábor Pap, Harmon Nine, Gabor Karsai, Michael R. Lowry, Corina S. Pasareanu, Thomas Pressburger : Rapid property specification and checking for model-based formalisms. International Symposium on Rapid System Prototyping 2011 : 121-127  (2011)
  • Matheus Souza, Mateus Borges, Marcelo d'Amorim, Corina S. Pasareanu: CORAL: Solving Complex Constraints for Symbolic PathFinder. NASA Formal Methods 2011 : 359-374 (2011)
  • Dimitra Giannakopoulou, Corina S. Pasareanu: Context Synthesis. SFM 2011 : 191-216  (2011)
  • Manuela L. Bujorianu  Michael Fisher, Corina S. Pasareanu: Preface. Ann. Math. Artif. Intell. 63 (1): 1-3 (2011
  • Corina S. Pasareanu: New results in software model checking and analysis. STTT 13 (1): 1-2 (2011)
  • Arnaud Venet. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Proceedings of the 3rd International Symposium on Static Analysis SAS’96, Aachen, Germany. Lecture Notes in Computer Science, pages 366-382, volume 1145, Springer 1996.
  • Arnaud Venet. Nonuniform Alias Analysis of Recursive Data Structures and Arrays. In Proceedings of the 9th International Symposium on Static Analysis SAS’02, Madrid, Spain. Lecture Notes in Computer Science, pages 36-51, volume 2477, Springer 2002.
  • G. Brat and R. Klemm. Static Analysis of the Mars Exploration Rover flight software. In the 1st International Space Mission Challenge for Information Technology, pp. 321-326. Pasadena, California, July 2003.
  • Arnaud Venet, Guillaume Brat. Precise and Efficient Static Array Bound Checking for Large Embedded C Programs. In Proceedings of the International Conference on Programming Language Design and Implementation, PLDI’04, Washington DC, USA, pages 231-242.
  • Arnaud Venet. A Scalable Nonuniform Pointer Analysis for Embedded Programs. In Proceedings of the International Static Analysis Symposium, SAS 04, Verona, Italy. Lecture Notes in Computer Science, pages 149-164, volume 3148, Springer 2004.
  • Guillaume Brat and Arnaud Venet. Precise and Scalable Static Program Analysis of NASA Flight Software. In Proceedings of the IEEE Aerospace Conference, Big Sky, MT, March, 2005.
  • Guillaume Brat, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Richard Washington, Willem Visser. Experimental Evaluation of Verification and Validation Tools on Martian Rover Software. In Formal Methods in Systems Design Journal, Volume 25, September 2005.
  • S. Thompson, A. Mycroft, G. Brat and A. Venet. Automatic In-Flight Repair of FPGA Cosmic Ray Damage. In Proceedings of the 1st Disruption in Space Symposium, Marseille, July, 2005.
  • Arnaud Venet. Towards the Integration of Symbolic and Numerical Static Analysis.  In Proceedings of the Conference on Verified Software: Theories, Tools, Experiments, VSTTE’05, Zurich, 10-14 October 2005.
  • John Anton, Eric Bush, Allen Goldberg, Klaus Havelund, Doug Smith, and Arnaud Venet. Towards the Industrial Scale Development of Custom Static Analyzers. In Proceedings of the NIST Static Analysis Summit, Gaithersburg, MD, USA 2006.
  • Eric Féron and Arnaud Venet. Static Stability Analysis of Embedded, Autocoded Software. In Proceedings of the Workshop on Verified Software: Tools, Theories, Experiments, VSTTE’06, Seattle, 2006. Microsoft Research Report.
  • Arnaud Venet. Static Analysis for High Assurance and Security. NSA Conference on High Confidence Software and Systems, Linthicum Heights, MD, USA 2007.
  • Arnaud Venet. A Practical Approach to Formal Software Verification by Static Analysis. In Ada Letters XXVIII, 1 (Apr. 2008), 92-95.
  • Sarah Thompson, Guillaume Brat and Arnaud Venet. Software Model Checking of ARINC-653 Flight Code with MCP. In Proceedings of the Second NASA Formal Methods Symposium, Washington D.C., USA 2010.
  • Arnaud Venet and Michael Lowry. Static Analysis for Software Assurance: Soundness, Scalability and Adaptiveness. In Proceedings of the Workshop on the Future of Software Engineering Research (FoSER'2010), Santa Fe, NM, USA 2010, pages 393-396.