• Compositional Verification
• Model Checking (including Java PathFinder, Livingstone PathFinder, MCP)
• Autocode Verification
• V&V of Neural Net and Adaptive Systems
• Runtime Analysis (including Java PathExplorer)
• Static Analysis (including C Global Surveyor)
• Testing and Analysis
• Theorem Proving
• Advanced Validation Testing
• Miscellaneous

Compositional Verification

Misty Davies, Viswanath Raman, Corina Pasareanu, "Symbolic Execution Enhanced System Testing," Verified Software: Theories, Tools and Experiments 2012, Philadelphia, PA, 29 January 2012.
[paper (PDF, 45K)]

Rishab Singh, Dimitra Giannakopoulou, Corina Pasareanu, "Learning Component Interfaces with May and Must Abstractions,” 22nd International Conference on Computer Aided Verification (CAV '10), Edinburgh, Scotland, July 15-19, 2010.
[paper (external link; PDF, 266.5K)]

Dimitra Giannakopoulou, Corina Pasareanu, "Interface Generation and Compositional Verification in JavaPathfinder," Fundamental Approaches to Software Engineering (FASE 2009), York, UK, Mar. 22 - 29, 2009.
[paper (PDF, 232K)]

Suzette Person, Matthew Dwyer, Sebastian Elbaum, Corina Pasareanu, "Differential Symbolic Execution," 16th International Symposium on the Foundations of Software Engineering, Atlanta, GA, Nov. 9-14 2008.
[paper (external link, PDF, 1.4M)]

Dimitra Giannakopoulou, Corina Pasareanu, "Learning Techniques for Compositional Reasoning," Journal of Formal Methods in System Design, pp. 173-174, Volume 32, Number 3, Springer,June 2008.
[paper (external link)]

Mihaela Gheorghiu, Corina Pasareanu, Dimitra Giannakopoulou, "Automated Assume-Guarantee Reasoning by Abstraction Refinement," Proc. 20th International Conference on Computer Aided Verification (CAV 2008), Princeton, USA , Jun. 19, 2008.
[paper (PDF, 232K)]

Corina Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson Cobleigh, Howard Barringer, "Learning to Divide & Conquer: applying the L* algorithm to automate assume-guarantee reasoning," Formal Methods in System Design, Volume 32,Issue 3, Pages: 175 - 205, June 2008.
[paper (external link, PDF, 305K)]

Michael Emmi, Corina Pasareanu, Dimitra Giannakopoulou, "Assume Guarantee Verification for Interface Automata," Proc. 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008.
[paper (PDF, 230K)]

Guillaume Brat, "Software Verification for Space Applications Part II: Autonomous Systems," Proc. Universite Catholique De Vouvain Graduate Seminar (Moves), Namur, Belgium, Jun 12, 2007.
[presentation (PDF, 620K)]

Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina Pasareanu, "Refining Interface Alphabets for Compositional Verification," Proc. TACAS'07: Thirteenth Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Braga, Portugal, Mar. 24- Apr. 1, 2007.
[paper (PDF, 332K)]

Dimitra Giannakopoulou, Corina Pasareanu, "Towards a Compositional SPIN," Proc. SPIN' 06: 13th International Workshop on Model Checking of Software, Vienna, Austria, Mar. 30 - Apr. 1st, 2006.
[paper (PDF, 252K)]

Colin Blundell, Dimitra Giannakopoulou, Corina Pasareanu, "Assume-Guarantee Testing," Proc. SAVCBS'05: 4th Workshop on Specification and Verification of Component-Based Systems, Lisbon, Portugal, pp. 7-14, Sep. 5 - 6, 2005.
[paper (PDF, 469K)]

Dimitra Giannakopoulou, Corina Pasareanu, "Learning-Based Assume-Guarantee Verification," Proc. SPIN'05: 12th Int'l Workshop on Model Checking of Software, San Francisco, CA, pp. 282-287, Aug. 22-24, 2005.
[paper (PDF, 178K)]

Dimitra Giannakopoulou, Corina Pasareanu, Michael Lowry, Rich Washington, "Lifecycle Verification of the NASA Ames K9 Rover Executive," Proc. VVPS'05: Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems, Monterey, CA, Jun. 6-7, 2005.
[paper(PDF, 168K)]

Jamieson Cobleigh, Dimitra Giannakopoulou, Corina Pasareanu, "Assume-guarantee Verification of Source Code with Design-Level Assumptions," Proc. ICSE'04: 26th Int'l Conf. on Software Engineering, Edinburgh, Scotland, pp. 211-220, May 23-28, 2004.
[paper ( PDF, 107K)]

Howard Barringer, Dimitra Giannakopoulou, Corina Pasareanu, "Component Verification with Automatically Generated Assumptions," Journal of Automated Software Engineering,vol. 11, pp. 93-98, Jan. 2004.
[paper ( PDF, 282K)]
[presentation ( PPT, 288K)]

Howard Barringer, Dimitra Giannakopoulou, Corina Pasareanu, "Proof Rules for Automated Compositional Verification through Learning," Proc. SAVCBS'03: 2nd Workshop on Specification and Verification of the Component-Based Systems, Helsinki, Finland, pp. 14-21, Sep. 1, 2003.
[paper ( PDF, 162K)]

Sagar Chaki, Edmund Sagar, Dimitra Giannakopoulou, Corina Pasareanu, CM SEI: "Abstraction and Assume-guarantee Reasoning for Automated Software Verification," RIACS Tech Report, Mar. 18, 2005.
[paper (PDF, 219K)]

Jamieson Cobleigh, Dimitra Giannakopoulou, and Corina Pasareanu, "Learning Assumptions for Compositional Verification," Proc. TACAS'03: 9th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS vol. 2619, Warsaw, Poland, pp. 331-346, Apr. 7-11, 2003.
[paper ( PDF, 191K)]

Howard Barringer, Dimitra Giannakopoulou, Corina Pasareanu, "Assumption Generation for Software Component Verification," Proc. ASE'02: 17th IEEE Int'l Conf. Automated Software Engineering, Edinburgh, Scotland, pp. 3-12, Sep. 23-27, 2002.
[papers ( PDF, 115K)]

Corina Pasareanu, "DEOS Kernel: Environment Modeling using LTL Assumptions," NASA Ames Technical Report #NASA-ARC-IC-2000-196, July 2000.
[paper ( PDF, 175K)]

Back to Top

Model Checking (including Java PathFinder, Livingstone PathFinder, MCP)

Matheus Souza, Mateus Borges, Marcelo d'Amorim, Corina Pasareanu, "CORAL: Solving Comples Constraints for Symbolic PathFinder," Lecture Notes in Computer Science, Springer, 2011, Volume 6617/2011, pp. 359-374.
[paper (External Link)]

Corina Pasareanu, Neha Rungta, "Symbolic Pathfinder: Symbolic Execution of Java bytecode," International Conference on Automated Software Engineering (ASE '10) Antwerp, Belgium, Aug 30 - Sep 2 2010.
[paper (PDF, 334K)]

Karen Gundy-Burlet, Sarah Thompson, and Misty Davies, "Hybrid Decompositional Verification for Discovering Failures in Adaptive Flight Control Systems,” Infotech@Aerospace (I@A '10), Atlanta, Georgia, Apr 20 - 22, 2010.
[paper (PDF, 470K)]

Kristin Rozier, "Linear Temporal Logic Symbolic Model Checking," Computer Science Review, Elsevier, Feb. 10, 2010.
[paper (PDF, 3.87 MB)]

Saswat Anand, Corina Pasareanu, Willem Visser, "Symbolic Execution with Abstraction," Software Tools for Technology Transfer(STTT) pp.53-67, Volume 11, Number 1, Springer, February, 2009.
[paper (external link, PDF, 348K)]

Michael Lowry, "Intelligent Software Engineering Tools for NASA's Crew Exploration Vehicle," Proc. ISMIS 2008, Toronto, Canada, May 20-23, 2008.
[paper (PDF, 335K)]

Peter C. Mehlitz, "Trust Your Model - Verifying Aerospace System Models with Java™ Pathfinder," Proc. IEEE Aerospace Conf. '08, Big Sky, MT, Mar. 1-8, 2008.
[paper ( PDF, 900K)]

Sarah Thompson, Guillaume Brat, "Verification of C++ Flight Software with the MCP Model Checker," Proc. IEEE Aerospace Conf. '08, Big Sky, MT, Mar. 1-8, 2008.
[paper (PDF, 353K)]

Masoud Mansouri-Samani, Peter Mehlitz, Corina Pasareanu, John Penix, Guillaume Brat, Lawrence Markosian, Owen O'Malley, Thomas Pressburger, and Willem Visser, Program Model Checking: a Practitioner's Guide, NASA/TM-2008-214577, January 2008.
[Available from http://sarpresults.ivv.nasa.gov/]

Corina Pasareanu, Willem Visser, "Symbolic Execution and Model Checking for Testing," Proc. HVC'07: Haifa Verification Conference 2007, Haifa, Israel, pp 17-18, Oct. 23 - 25, 2007
[paper (PDF, 753K)]

Guillaume Brat, "Software Verification for Space Applications Part II: Autonomous Systems," Proc. Universite Catholique De Vouvain Graduate Seminar (Moves), Namur, Belgium, Jun 12, 2007.
[paper (PDF, 620K)]

Saswat Anand, Corina S. Pasareanu, Willem Visser, "JPF-SE: A Symbolic Execution Extension to Java PathFinder," Proc. TACAS'07: Thirteenth Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Braga, Portugal, Mar. 24- Apr. 1, 2007.
[paper (PDF, 240K)]

Larry Markosian, Masoud Mansouri-Samani, Peter Mehlitz, Thomas Pressburger, "Program Model Checking Using Design-for-Verification: NASA Flight Software Case Study," Proc. IEEE Aerospace Conf.'07, Big Sky, MT, Mar. 3-10, 2007.
[paper (PDF, 426K)]

Corina S. Pasareanu, Radek Pelanek, Willem Visser, "Predicate Abstraction with Under-Approximation Refinement," Logical Methods in Computer Science, Volume 3, Issue 1, pp. 1-22, Braunschweig, Germany, Feb. 26, 2007.
[paper (PDF, 288K)]

Vandi Verma, Ari Jonsson, Corina Pasareanu, Michael Iatauro, "Tool and Language support for Robust Spacecraft Control and Operations," Proc. AIAA SPACE'06: The Value Proposition for Space Security, Discovery, Prosperity , San Jose, CA, Sep. 19-21, 2006.

Willem Visser, Corina S. Pasareanu, Radek Pelanek, "Test Input Generation for Java Containers using State Matching," Proc. ISSTA'06: Int'l Symposium on Software Testing and Analysis, Portland, Maine, Jul. 18-20, 2006.
[paper (PDF, 150K)]

Saswat Anand, Corina S. Pasareanu, Willem Visser, "Symbolic Execution with Abstract Subsumption Checking," Proc. SPIN'06: 13th Int'l Workshop on Model Checking of Software, Vienna, Austria, Mar. 30 - Apr. 1st, 2006.
[paper (PDF, 319K)]

Willem Visser, Corina S. Pasareanu, Radek Pelanek, "Test Input Generation for Red Black Trees using Abstraction," Proc. ASE'05: 20th IEEE/ACM Int'l Conf. on Automated Engineering, Long Beach, CA, pp. 414-417, Nov. 7-11, 2005. [paper (PDF, 72K)]

Gary Lindstrom, Peter Mehlitz, Willem Visser, "Model Checking Real Time Java Using Java PathFinder," Proc. ATVA'05: 3rd Int'l Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan, pp. 444-456, Oct. 4-7, 2005.
[paper (PDF, 229K)]

Corina Pasareanu, Radek Pelanek, Willem Visser, "Concrete Model Checking with Abstract Matching and Refinement," Proc. CAV'05: 17th Int'l Conf. on Computer Aided Verification, Edinburgh, Scotland, pp. 52-66, Jul. 6-10, 2005.
[paper (PDF, 258K)]

John Penix, Willem Visser, Corina Pasareanu, Eric Engstorm, Aaron Larson, Nicholas Weininger, "Verifying Time Partitioning in the DEOS Scheduling Kernel," Formal Methods in Systems Design, vol. 26, no. 2, pp. 103-135, Mar. 2005.
[paper (PDF, 567K)]

Alex Groce, Willem Visser, "Heuristics for Model Checking Java Programs," Int'l Journal on Software Tools for Technology Transfer, vol. 6, no. 4, pp. 260-276, Dec. 2004.
[paper (PDF, 465K)]

Guillaume Brat, Rich Washington, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Formal Methods in System Design, vol. 25, no. 2-3, pp. 167-198, Sep. - Nov. 2004.
[paper (PDF, 577K)]

Matthew Dwyer, Robby, Oksana Tkachuk, Willem Visser, "Analyzing Interaction Orderings with Model Checking," Proc. ASE'05: 19th Automated Software Engineering Conference, Linz, Austria, pp.154-163, Sep. 20-25, 2004.
[paper (PDF, 167K)]

Rafael H.Bordini, Michael Fisher, Willem Visser, Michael Wooldridge, "State-space Reduction Techniques in Agent Verification," Proc. AAMAS'04: 3rd Int'l Joint Conf. on Autonomous Agents and Multi-Agent Systems, New York, NY, pp. 896-903, Jul. 19-23, 2004.
[paper (PDF, 180K)]

Willem Visser, Corina Pasareanu, Sarfraz Khurshid, "Test Input Generation with Java PathFinder," Proc. ISSTA 2004: Int'l Symp. on Software Testing and Analysis,vol. 29, no. 4, pp. 97-107, Boston, MA., Jul. 14, 2004.
[paper ( PDF, 220K)]

Corina Pasareanu, Willem Visser, "Verification of Java Programs Using Symbolic Execution and Invariant Generation," Proc. SPIN2004: 11th Int'l SPIN Workshop, Springer LNCS, vol. 2989, Barcelona, Spain, pp. 164-181, Apr. 1-3, 2004.
[paper ( PDF, 1.1M)]

Tony Lindsey, Charles Pecheur, "Simulation-Based Verification of Autonomous Controllers with Livingstone PathFinder," Proc. TACAS'04: Tenth Int'l Conf. on Tools And Algorithms For The Construction And Analysis Of Systems, Springer LNCS, vol. 2988, Barcelona, Spain, pp. 357-371, Mar. 29 to Apr. 2, 2004.
[paper ( PDF, 616K)]

Corina Pasareanu, Matthew Dwyer, Willem Visser, "Finding Feasible Abstract Counter-examples," Int'l Journal on Software Tools for Technology Transfer, vol. 5, no. 1, pp. 34-48, Nov. 2003.
[paper ( PDF, 251)]

Dimitra Giannakopoulou, Jeff Magee, "Fluent Model Checking for Event-Based Systems," Proc. ESEC/FSE 2003: 4th Joint Meeting of the European Software Engineering Conf. and ACM SIGSOFT Symposium on the Foundations of Software Engineering, Helsinki, Finland, pp. 14-21, Sep. 1-5, 2003.
[paper ( PDF, 249K)]

Alessandro Cimatti, Charles Pecheur, Roberto Cavada, "Formal Verification of Diagnosability via Symbolic Model Checking," Proc. IJCAI 2003: 18th Int'l Joint Conf. on Artificial Intelligence, Acapulco, Mexico, pp. 501-503, Aug. 9-15, 2003.
[papers ( PDF, 125K)]

Rafael Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael Wooldridge, "Model Checking Multi-Agent Programs with CASP" Proc. CAV'03: 15th Computer-Aided Verification Conference, Springer LNCS, vol. 2725, Boulder, CO., pp. 110-113, Jul. 8-12, 2003.
[papers ( PDF, 279K)]

Masoud Mansouri-Samani, Peter Mehlitz, Lawrence Markosian, Owen O'Malley, Dale Martin, Lantz Moore, John Penix, Willem Visser, "Propel: Tools and Methods for Practical Source Code Model Checking," Proc. DSN'03: Int'l Conf. on Dependable Systems and Networks, San Francisco, CA, Jun. 22-25, 2003.
[PDF, 70K]

Tony Lindsey, Charles Pecheur, "Simulation-Based Verification of Livingstone Applications," Proc. DSN 2003: Int'l Conf. on Dependable Systems and Networks, San Francisco, CA, pp. 741-750, Jun. 22-25, 2003.
[papers ( PDF, 61K)]

Alex Groce, Willem Visser, "What Went Wrong: Explaining Counterexamples," Proc. SPIN 2003: 10th Int'l SPIN Workshop on Model Checking of Software, Springer LNCS, no. 2648, Portland, OR, pp. 121-135, May 9-10, 2003.
[papers ( PDF, 242K)]

Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, Flavio Lerda, "Model Checking Programs," Journal on Automated Software Engineering, vol. 10, no. 2, pp. 203-232, Apr. 2003.
[papers ( PDF, 206K)]

Sarfraz Khurshid, Corina Pasareanu, Willem Visser, "Generalized Symbolic Execution for Model Checking and Testing," Proc. TACAS 2003: 9th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, vol. 2619, Warsaw, Poland, pp. 553-568, Apr. 7-11, 2003.
[paper ( PDF, 286K)]

Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Michael Lowry, Corina S. Pasareanu, Arnaud Venet, Willem Visser, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Proc. SEI Software Model Checking Workshop, Formal Methods in System Design, vol. 25, issue 2, Pittsburgh, PA, pp. 167-198, Mar. 24, 2003.
[paper (PDF, 416K)]

John Hatcliff, Matthew Dwyer, Corina Pasareanu, Robby, "Foundations of the Bandera Abstraction Tools," Proc. Essence of Computation, Complexity, Analysis, Transformation, Feb. 10, 2003.
[paper (PDF, 467K)]

Dimitra Giannakopoulou, Flavio Lerda, "From States to Transitions: Improving translation of LTL Formulae to Buchi Automata," Proc. FORTE 2002: 22nd IFIP WG 6.1 Int'l Conf. on Formal Techniques for Networked and Distributed Systems, Springer LNCS, vol. 2529, pp. 308-326, Houston, TX, Nov. 11-14, 2002.
[paper ( PDF, 159K)]

Stacy Nelson, Charles Pecheur, "Formal Verification of a Next-Generation Space Shuttle," Proc. FAABS 2002: Second Workshop on Formal Aspects of Agent-Based Systems, Springer LNCS, vol. 2699, Greenbelt, MD, pp. 53-67, Oct. 28-30, 2002.
[paper ( PDF, 356 K)]

Klaus Havelund, Willem Visser, "Program Model Checking as a New Trend," Int'l Journal on Software Tools for Technology Transfer, Springer Heidelberg, vol. 4, no. 1, pp. 8-20, Oct. 2002.
[paper ( PDF, 201K)]

Charles Pecheur, Alessandro Cimatti, "Formal Verification of Diagnosablility via Symbolic Model Checking," Proc: MoChArt 2002: Workshop on Model Checking and Artificial Intelligence, Lyon, France, Jul. 22-23, 2002.
[papers ( PDF, 126K)]

Alex Groce, Willem Visser, "Model Checking Java Programs using Structural Heuristics," Proc. ISSTA 2002: Int'l Symp. on Software Testing and Analysis, Rome, Italy, pp. 12-21, Jul. 22-24, 2002.
[papers ( PDF, 964K)]

Alex Groce, Willem Visser, "Heuristics for Model Checking Java Programs," Proc. SPIN'02: 9th Int'l SPIN Workshop on Model Checking of Software, Grenoble, France, pp. 242-259, Apr. 11-13, 2002.
[papers ( PDF,1.8M)]

Steven Brown, Charles Pecheur, "Model-Based Verification of Diagnostic Systems," Proc. JANNAF Joint Meeting, Destin, FL, Apr. 8-12, 2002.
[paper ( PDF, 32K)]

Guillaume Brat, Willem Visser, "Combining Static Analysis and Model Checking for Software Analysis," Proc. ASE'01: 16th IEEE Int'l Conf. on Automated Software Engineering, San Diego, CA, pp. 262-272, Nov. 26-29, 2001.
[paper ( PDF, 91K)]

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN,"(modified), IEEE Transactions on Software Engineering, vol. 27, no. 8, pp. 749-765, Aug. 2001.
[papers ( PDF, 165K)]

Flavio Lerda, Willem Visser, "Addressing Dynamic Issues of Program Model Checking," Proc. SPIN'01: 8th Int'l SPIN Workshop on Model Checking of Software, Springer LNCS, vol. 2057, Toronto, Canada, pp. 80-102, May 19-20, 2001.
[papers ( PDF, 244K)]

Matthew Dwyer, John Hatcliff, Robby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, and Hongjun Zheng, "Tool-Supported Program Abstraction for Finite-State Verification," Proc. ICSE'01: 23rd Int'l Conf. on Software Engineering, Toronto, Canada, pp. 177-187, May 12-19, 2001.
[paper ( PDF, 99K)]

Corina Pasareanu, Matthew Dwyer, Willem Visser, "Finding Feasible Counter-examples when Model Checking Abstracted Java Programs," Proc. TACAS 2001: 7th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, vol. 2031, pp. 284-298, Apr. 2-6, 2001.
[paper ( PDF, 227K)]

Reid Simmons, Charles Pecheur, "Towards Automatic Verification of Autonomous Systems," Proc. IROS'00: 2000 IEEE/RSJ Int'l Conf. on Intelligent Robots and Systems, Takamatsu, Japan, Oct. 31 - Nov. 5 2000.
[paper ( PDF, 78K)]

Guillaume Brat, Klaus Havelund, SeungJoon Park, Willem Visser, "Model Checking Programs," Proc. ASE'00: 15th IEEE Int'l Conf. on Automated Software Engineering, Grenoble, France, pp. 3-11, Sep. 11-15, 2000.
[papers ( PDF, 70K)]

William Visser, SeungJoon Park, John Penix, "Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking," Proc. FMSP'00: 3rd ACM Workshop on Formal Methods in Software Practice, Portland, OR, pp. 3-13, Aug. 23-25, 2000.
[papers ( PDF, 163K)]

Willem Visser, SeungJoon Park, John Penix, "Applying Predicate Abstraction to Model Check Object-Oriented Programs," Proc. FMSP 2000: 3rd Workshop on Formal Methods in Software Practice, Aug. 22-25, 2000.
[papers ( PDF, 1.1M)]

Guillaume Brat, SeungJoon Park, Klaus Havelund, Willem Visser, "Java PathFinder-Second Generation of a Java Model Checker," Post-CAV Workshop on Advances in Verification, Jul. 20 2000.
[papers ( PDF, 159K)]

Klaus Havelund, Michael Lowry, SeungJoon Park, Charles Pecheur, John Penix, Willem Visser, Jonathan White, "Formal Analysis of the Remote Agent Before and After Flight," Proc. 5th NASA Langley Formal Methods Workshop, Williamsburg, VA, Jun. 13-15 2000.
[paper ( PDF, 97K)]

John Penix, Willem Visser, Eric Engstrom, Aaron Larson, Nicholas Weininger, "Verification of Time Partitioning in the DEOS Scheduler Kernel," Proc. 22nd Int'l Conf. on Software Engineering, Limerick, Ireland, pp. 488-497, Jun. 4-11 2000.
[paper ( PDF, 74K)]

Klaus Havelund, Tom Pressburger, "Model Checking Java Programs Using Java PathFinder," Int'l Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 366-381, Apr. 2000.
[paper ( PDF, 298K)]

Charles Pecheur, Reid Simmons, "From Livingstone to SMV: Formal Verification for Autonomous Spacecrafts," Proc. FAABS 2000: First Goddard Workshop on Formal Approaches to Agent-Based Systems, Springer LNCS, pp. 103-113, Apr. 5-7, 2000.

Lina Khatib, Nicola Muscettola, Klaus Havelund, "Verification of Plan Models Using UPPAAL," Proc. FAABS 2000: First Goddard Workshop on Formal Approaches to Agent-Based Systems, Springer LNCS, pp. 114-122, Apr. 5-7, 2000.
[paper (PDF, 128K)]

Reid Simmons, Charles Pecheur, "Automating Model Checking for Autonomous Systems," Proc. AAAI Spring Symp. on Real-Time Autonomous Systems, Palo Alto, CA, Mar. 20-22, 2000.

Klaus Havelund, Jens Skakkebaek, "Applying Model Checking in Java Verification," Proc. SPIN'99: 6th Int'l SPIN Workshop on Practical Aspects of Model Checking, Springer LNCS, vol. 1680, Toulouse, France, pp. 216-231, Sep. 21-24, 1999.

Daniel Clancy, William Larson, Charles Pecheur, Peter Engrand, Charles Goodrich, "Autonomous Control of an in-Situ Propellant Production Plant," Proc. of the Technology 2009 Nat'l Conf., Miami Beach, FL, Nov. 1-3, 1999.
[papers ( PDF, 435K)]

Anthony Gross, K.R. Sridhar, William Larson, Daniel Clancy, Charles Pecheur, Geoffrey Briggs, "Information Technology and Control Needs for In-Situ Resource Utilization," Proc. 50th IAF Congress, Amsterdam, Holland, Oct. 4-8, 1999.
[papers ( PDF, 791K)]

Willem Visser, Klaus Havelund, John Penix, "Adding Active Objects to SPIN," Proc. 5th Int'l SPIN Workshop on Theoretical Aspects of Model Checking, Trento, Italy, pp. 40-51, July 5, 1999.
[paper ( PDF, 196K)]

Richard Doyle, Douglas Bernard, Ed Riedel, Nicholas Rouquette, Jay Wyatt, Michael Lowry, Pandurang Nayak, "Autonomy and Software Technology on NASA's Deep Space One," IEEE Intelligent Systems, vol. 14, issue 3, pp. 10-15, May 1999.
[paper ( PDF, 1.6M)]

Klaus Havelund, Kim Larsen, Arne Skou, "Formal Verification of an Audio/Video Power Controller using the Real-Time Model Checker UPPAAL," Proc. ARTS'99: 5th Int'l AMAST Workshop on Real-Time and Probabilistic Systems, Springer LNCS, Bamberg, Germany, pp. 277-298, May 26-28, 1999.
[papers ( PDF, 159K)]
[tech reports ( PDF, 842K)]

Wray Buntine, Bernd Fisher, Klaus Havelund, Michael Lowry, Tom Pressburger, Steve Roach, Peter Robinson, Jeffrey Van Baalen, "Transformation Systems at NASA Ames," Proc. STS'99: Int'l Workshop on Software Transformation Systems, Los Angeles, CA, May 17, 1999.
[paper ( PDF, 154K)]

Michael Lowry, Daniel Dvorak, "Analytic Verification of Flight Software," IEEE Intelligent Systems, vol. 13, issue 5, pp. 45-49 Sep 1998.
[paper ( PDF, 755K)]

John Penix, Charles Pecheur, Klaus Havelund, "Using Model Checking to Validate AI Planner Domain Models," Proc. SEL98: 23rd Annual Software Engineering Workshop, Greenbelt, MD, Dec. 2-3 1998.
[papers ( PDF, 163K)]
[slides ( PowerPoint)]

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN," Proc. SPIN'98: 4th Int'l SPIN Workshop, vol. 27, issue 8, Paris, France, pp. 749-765, Nov. 2, 1998.
[papers ( PDF, 148K)]

Klaus Havelund, Michael Lowry, John Penix, "Formal Analysis of a Space Craft Controller using SPIN,"(extended version), NASA Ames Tech. Report, no. 1770, Nov. 1997.
[tech reports ( PDF, 443K)]

Michael Lowry, Mahadevan Subramaniam, "Abstraction for Analytic Verification of Concurrent Software Systems," Proc. SARA98: Symp. on Abstraction, Reformulation, and Approximation, Pacific Grove, CA., May 9-12, 1998.
[papers ( PDF, 194K)]

John Penix, Perry Alexander, Klaus Havelund, "Declarative Specification of Software Architectures," Proc. ASE'97: 12th IEEE Int'l Conf. on Automated Software Engineering, Incline Village, NV., pp. 201-208, Nov. 1-5, 1997.
[paper (PDF, 693K)]

Michael Lowry, Klaus Havelund, John Penix, "Verification and Validation of AI Systems that Control Deep-Space Spacecraft,"(revised), Proc. ISMIS'97: 10th Int'l Symp. on Methodologies for Intelligent Systems, Springer LNAI, vol. 1325, Charlotte, NC., pp. 35-47, Oct. 15-18, 1997. Springer-Verlag Lecture Notes in Artificial Intelligence, Vol. 1325.
[papers ( PDF, 33K)]

Back to Top

Autocode Verification

Ki Yung Ahn and Ewen Denney, "Testing First-Order Logic Axioms in Program Verification," 4th International Conference on Tests & Proofs (TAP 2010), Malaga, Spain, July 1 2010 .
[paper (PDF, 425K)]

Ewen Denney, "Synthesizing Verifiers for Synthesized Code," Dagstuhl Seminar on Software Synthesis, Schloß Dagstuhl, Germany, Mar. 01 - Aug. 01 2010.
[paper (link coming...)]

Ewen Denney, Bernd Fischer, "A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software," IEEE/ACM International Conference on Automated Software Engineering (ASE09), Auckland, New Zealand, Nov. 16th, 2009.
[paper (PDF, 286K)]

Ewen Denney, Bernd Fischer, "Generating code review documentation for auto-generated mission-critical software" Proc. Third IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT), Pasadena, California, Jul. 19-23, 2009.
[paper (PDF, 1.5M)]

Ewen Denney, Bernd Fischer, "Generating Customized Verifiers for Automatically Generated Code". In Proc. GPCE '08: 7th International Conference on Generative Programming and Component Engineering. Nashville, Tennessee , Oct. 19-23, 2008.
[paper (PDF, 181K)]

Nurlida Basir, Ewen Denney, Bernd Fischer, "Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information".Proc. SAFECOMP '08: The 27th International Conference on Computer Safety, Reliability and Security. Newcastle, England, Sept. 22-25 2008.
[paper (PDF, 129K)]

Ewen Denney, "Generating Customized Verifiers for Automatically Generated Code," Proc. Seventh International Conference on Generative Programming and Component Engineering , Nashville, Tennessee, Jul. 28, 2008.
[paper (PDF, 175K)]

Nurlida Basir, Ewen Denney, Bernd Fischer, "Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code," Proc. SafeCert '08: International Workshop on the Certification of Safety-Critical Software Controlled Systems, Budapest, Hungary, Mar. 29, 2008.
[paper (PDF, 90K)]

Ewen Denney, Steven Trac, "A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code," Proc. IEEE Aerospace Conf., Big Sky, MT, Mar. 1-8, 2008.
[paper (PDF, 1.87M)]

Ewen Denney, Bernd Fischer, "A generic annotation inference algorithm for the safety certification of automatically generated code," Proc. GPCE'06: 5th Int'l Conf. on Generative Programming and Component Engineering, Portland , Oregon, Oct. 22-26, 2006.
[paper (PDF, 127K)]

Ewen Denney, Bernd Fischer, "Annotation inference for the safety certification automatically generated code," Proc. ASE'06: 21st IEEE/ACM Int'l Conf. on Automated Software Engineering, Tokyo, Japan, Sep. 18-22, 2006.
[paper (PDF, 239K)]

Back to Top

V&V of Neural Net and Adaptive Systems

Johann Schumann, Applications of Neural Networks in High Assurance Systems, Springer, Mar. 1, 2010.
[book (external link)]

Johann Schumann, "Verification & Validation of Adaptive Systems: Course Presentation," Lecture Series "Discrete Mathmatics and Logic" UNESCO, Tunis, Tunisia, Apr. 7-11, 2008.
[paper (PDF, 137K)]

Stephen Jacklin, Johann Schumann, Kurt Guenther, John Bosworth, "Case Study:Test Results of a Tool and Method for In-Flight, Adaptive Control System Verification on a NASA F-15 Flight Research Aircraft," Proc. 7th World Congress on Computational Mechanics, Los Angeles, California, Jul 16-21, 2006.
[paper (PDF, 254K)]

Pramod Gupta, Kurt Guenther, John Hodgkinson, Stephen Jacklin, Michael Richard, Johann Schumann, Fola Soares, "Performance Monitoring and Assessment of Neuro-Adaptive Controllers for Aerospace Applications Using a Bayesian Approach," Proc. AIAA Guidance, Navigation, and control conference and exihibt, San Francisco, CA, Aug. 15-18, 2005.
[paper (PDF, 94K)]

Stephen Jacklin, Pramod Gupta, Johann Schumann, Michael Richard, Kurt Guenther, Fola Soares, "Towards Development of Advanced Verification and Validation Tools for the Certification of Learning Systems in Aerospace Applications," Proc. AIAA Infotech, Arlington, Virginia, Sept. 26-29 2005.
[paper (PDF, 219K)]

Johann Schumann, Pramod Gupta, Stephen Jacklin, "Toward Verification and Validation of Adaptive Aircraft Controllers," Proc. IEEE Aerospace Conf., Big Sky, MT, CD-ROM, March 2005.
[paper (PDF, 235K)]

Stephen Jacklin, Michael Lowry, Johann Schumann, Pramod Gupta, John Bosworth, Eddie Zavala John Kelly, Kelly Hayhurst, Celeste Belcastro, Christine Belcastro, "Verification, Validation and Certification Challenges for Adaptive Flight Control Systems Software," Proc. AIAA Guidance, Navigation, and Control Conference and Exhibit, Providenec, RI, CD-ROM, Aug. 16-19 2004.

Johann Schumann, Pramod Gupta, "Monitoring the Performance of a neuro-adaptive Controller," Proc. MAXENT'04: 24th Int'l Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Munich, Germany, pp. 289-296, Jul. 25-30, 2004.
[paper (PDF, 238K)]

Pramod Gupta, Ken Loparo, Dale Mackall, Johann Schumann, Fola Soares, "Verification and Validation Methodology of Real-Time Adaptive Neural Networks for Aerospace Applications," Proc. CIMCA'04: Int'l Conf. on Computational Intelligence for Modeling, Control and Automation, Gold Coast, Australia, Jul. 12-14, 2004.
[paper (PDF, 1.2M)]

Johann Schumann, Pramod Gupta, Stacy Nelson, "On Verification and Validation of Neural Network Based Controllers," Proc. EANN'03: Engineering Applications of Neural Networks, Malaga, Spain, pp. 84-92, Sep. 8-10, 2003.

Stacy Nelson, Johann Schumann, "Toward V&V of Neural Network Based Controllers," Proc. WOSS'02: Workshop on Self-Healing Systems,Charleston SC., pp. 67-72, Nov. 18-19, 2002.
[papers ( PDF, 255K)]

Back to Top

Runtime Analysis (including Java PathExplorer)

Guillaume Brat, Rich Washington, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Formal Methods in System Design, vol. 25, no. 2-3, pp. 167-198, Sep. - Nov., 2004.
[paper ( PDF, 416K]

Klaus Havelund and Grigore Rosu, "An Overview of the Runtime Verification Tool Java PathExplorer," Formal Methods in Systems Design, vol. 24, no. 2, pp. 189-215, Springer, March 2004.
[paper ( external link, PDF, 295K]

Howard Barringer, Allen Goldberg, Klaus Havelund, Kourshik Sen, "Rule-Based Runtime Verification," Proc. VMCAI'04: Fifth Int'l Conf. on Verification, Model Checking and Abstract Interpretation,Springer LNCS, vol. 2937, Venice, Italy, pp. 44-57, Jan. 11-13, 2004.
[paper ( PDF, 100K)]

Guillaume Brat, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, Rich Washington, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Proc. SEI Software Model Checking Workshop, Pittsburgh, PA., pp. 167-198, Mar. 24, 2003.
[paper ( PDF, 416K]

Cyrille Artho, Klaus Havelund, Armin Biere, "High-Level Data Races," Proc. VVEIS'03: 1st Int'l Workshop on Verification and Validation of Enterprise Information Systems,Angers, France, Apr. 22, 2003.
[paper ( PDF, 64K)]

Cyrille Artho, Doron Drusinsky, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Grigore Rosu, Willem Visser, "Experiments with Test Case Generation and Runtime Analysis," Proc. ASM 2003: 10th Int'l Workshop on Abstract State Machines, Springer LNCS, vol. 2589, Taormina, Italy, pp. 87-107, Mar. 3-7, 2003.
[paper ( PDF, 241K)]

Robert Filman, Klaus Havelund, "Source-Code Instrumentation and Quantification of Events," Proc. FOAL'02: Foundations of Aspect-Oriented Languages, Enschede, The Netherlands, pp. 45-53, Apr. 22, 2002.
[paper ( PDF, 65K)]

Klaus Havelund, Grigore Rosu, "Synthesizing Monitors for Safety Properties," Proc. TACAS'02: Int'l Conf. on Tools and Algorithms for Construction and Analysis of Systems, Springer LNCS, vol. 2280, Grenoble, France, pp. 342-356, Apr. 6-14, 2002.
[paper ( PDF, 223K)]

Dimitra Giannakopoulou, Klaus Havelund, "Automata-Based Verification of Temporal Properties on Running Programs," Proc. ASE'01: 16th IEEE Int'l Conf. on Automated Software Engineering, Coronado Island, CA., pp. 412-423, Nov. 26-29, 2001.
[paper ( PDF, 382K)]

Klaus Havelund, Grigore Rosu, "Monitoring Programs using Rewriting," Proc. ASE'01: 16th Int'l Conf. on Automated Software Engineering, Coronado Island, CA., pp. 135-143, Nov. 26-29, 2001.
[paper ( PDF, 111K)]

Klaus Havelund, Grigore Rosu, "Monitoring Java Programs with Java PathExplorer," Proc. RV'01: 1st Workshop on Runtime Verification, Paris, France, July 23, 2001. Electronic Notes in Theoretical Computer Science (ENTCS), vol. 55, issue 2, pp. 200-217, Springer, October 2001.
[paper ( PDF, 237K)]

Klaus Havelund, Scott Johnson, Grigore Rosu, "Specification and Error Pattern Based Program Monitoring," European Space Agency Workshop on On-Board Autonomy, Noordwijk, Holland, pp. 323-330, Oct. 17-19, 2001.
[paper ( PDF, 227K)]

Klaus Havelund, Grigore Rosu, "Java PathExplorer-A Runtime Verification Tool," Proc. ISAIRAS'01: 6th Int'l Symp. on AI, Robotics and Automation in Space, Nordwijk, The Netherlands, pp. 31-49, May 2001.
[paper ( PDF, 173K)]

Klaus Havelund, Grigore Rosu, "Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae," RIACS Technical Report, pp. 45-49, May 1-15, 2001.
[paper ( PDF, 187K)]

Klaus Havelund, Grigore Rosu, "Testing Linear Temporal Logic Formulae on Finite Execution Traces," RIACS Technical Report, pp. 101-127, May 1-8 2001.
[paper ( PDF, 260K)]

Klaus Havelund, "Using Runtime Analysis to Guide Model Checking of Java Programs," Proc. SPIN'00: 7th Int'l SPIN Workshop Springer LNCS, vol. 1885, Stanford, California, pp. 245-264, Aug. 30 - Sep. 1, 2000.
[paper ( PDF, 272)]

John Penix, Charles Pecheur, Klaus Havelund, "Using Model Checking to Validate AI Planner Domain Models," Proc. SEL'98: 23rd Annual Software Engineering Workshop, NASA Goddard, Dec.2-3 1998.
[papers ( PDF, 163K)]
[slides ( PowerPoint)]

Michael Lowry, Daniel Dvorak, "Analytic Verification of Flight Software," IEEE Intelligent Systems, vol. 13, issue 5, pp. 45-49 Sep. 1998.
[paper ( PDF, 756K)]

Back to Top

Static Analysis (including C Global Surveyor)

Guillaume Brat, "Experiences in the Static Analysis of Embedded Software," Proc. AFADL '07, Namur, Namur, Jun. 13-15, 2007.
[paper (PDF, 1.31M)]

Guillaume Brat, "Software Verification for Space Applications Part I: Static Analysis," Proc. Universite Catholique De Vouvain Graduate Seminar (Moves), Namur, Belgium, Jun 12, 2007.
[paper (PDF, 1.13M)]

Guillaume Brat, Arnaud Venet, "Precise and Scalable Static Program Analysis of NASA Flight Software," IEEE Aerospace Conference, Big Sky, MT, March, 2005.
[paper (PDF, 170K)]

Guillaume Brat, Rich Washington, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Formal Methods in System Design, vol. 25, no. 2-3, pp. 167-198, Sep. - Nov. 2004.
[paper ( PDF, 416K]

Arnaud Venet, Guillaume Brat, "Precise and Efficient Static Array Bound Checking for Large Embedded C Programs," Proc. PLDI'04: ACM SIGPLAN Conf. on Programming Language Design and Implementation, Washington DC, USA, pp. 231-242, June 9-11, 2004.
[paper ( PDF,180K)]

Cyrille Artho, Klaus Havelund, "Applying Jlint to Space Exploration Software," Proc. VMCAI'04: 5th Int'l Conf. on Verification, Model Checking and Abstract Interpretation, Venice, Italy, pp. 597-607, Jan. 11-13, 2004.
[paper ( PDF, 74K)]

Guillaume Brat, Roger Klemm, "Static Analysis of the Mars Exploration Rover flight software," Proc. 1st Int'l Space Mission Challenge for Information Technology, Pasadena, CA., pp. 321-326, Oct. 15-18, 2003.
[paper ( PDF, 140K)]

Guillaume Brat, Arnaud Venet, "Static Program Analysis Using Abstract Interpretation,"(unpublished tutorial) Proc. ASE'03: 18th IEEE Int'l Conf. on Automated Software Engineering, Montreal, Canada, Oct. 6-10, 2003.
[presentations ( PPT, 330K),( PDF, 1.1M)]

Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Michael Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software," Proc. SEI Software Model Checking Workshop, Pittsburgh, PA., Mar. 24, 2003.
[paper ( PDF, 577K]

Michael Lowry, Thomas Pressburger, Grigore Rosu, "Certifying Domain-Specific Policies," Proc. ASE'01: 16th IEEE Int'l Conf. on Automated Software Engineering, Coronado Island, CA., pp. 81-90, Nov. 26-29, 2001.
[paper ( PDF, 122K)]

Guillaume Brat, Willem Visser, "Combining Static Analysis and Model Checking for Software Analysis," Proc. ASE'01: 16th IEEE Int'l Conf. on Automated Software Engineering, Coronado Island, CA., pp. 262-272, Nov. 26-29, 2001.
[paper ( PDF, 91K)]

Bernd Fischer, Grigore Rosu, "Interpreting Abstract Interpretations in Membership Equational Logic," Proc. RULE'02: Int'l Workshop on Rule-Based Programming, Electronic Notes in Theoretical Computer Science, vol. 59, issue 4, pp. 1-15, Nov. 4, 2001.
[papers ( PDF, 277K)]

Arnaud Venet, "Abstract Cofibered Domains: Application to the Analysis of Untyped Programs," Proc. SAS'96: Static Analysis, Third Int'l Symp., Springer LNCS, no. 1145, pp. 366-382, Sep. 24-26, 1996.
[papers ( PDF, 911K)]

Back to Top

Testing and Analysis

Corina Pasareanu, "Parallel Symbolic Execution for Structural Test Generation," International Symposium on Software Testing and Analysis (ISSTA '10), Trento, Italy Jul. 12, 2010.
[paper (external link, PDF, 469 KB)]

Matt Staats, Corina Pasareanu, "A Test Generation Framework for Distributed Fault-Tolerant Algorithms," Automated Formal Methods (AFM '09) , Grenoble, France, June 27, 2009.
[paper (link coming...)]

CorinaPasareanu, Peter Mehlitz, David Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person, Mark Pape, "Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software," Proc. ISSTA’08: International Symposium on Software Testing and Analysis, Seattle, WA, Jul. 20-24, 2008.
[paper (PDF, 670K)]

Michael Lowry, "Intelligent Software Engineering Tools for NASA's Crew Exploration Vehicle," Proc. ISMIS 2008, Toronto, Canada, May 20-23, 2008.
[paper (PDF, 335K)]

Guillaume Brat, "Verification of Model-based Software Systems for Space Applications," Proc. NASA Fault Management Workshop, New Orleans, Louisiana, Apr. 14, 2008.
[paper (PDF, 1.28M)]

David Bushnell, Corina Pasareanu, Ryan Mackey, "Automatic Test Generation for Flight Software," Proc. NASA Planetary Spacecraft Fault Management Workshop, New Orleans, Louisiana, Apr. 13, 2008.
[paper (PDF, 261K)]

Karen Gundy-Burlet, Johann Schumann, Tim Menzies, and Tony Barrett, "Parametric Analysis of Antares Re-Entry Guidance Algorithms using Advanced Test Generation and Data Analysis," Proc. i-SAIRAS'08: 9th International Symposium on Artificial Intelligence, Robotics, and Automation in Space , Universal City, California, February 25-29, 2008.
[paper (PDF, 451K)]

Aaron Tomb, Guillaume Brat, and Willem Visser, "Variably interprocedural program analysis for runtime error detection," Proc. 2007 International symposium on Software Testing and Analysis ISSTA '07, London, UK, Jul. 9~12, 2007; pp 97-107
[paper (external link, PDF, 270K)]

Franco Raimondi, Charles Pecheur, Guillaume Brat, "Testing Planning Domains (Without Model Checkers)," Proc. Third Workshop on Model-Based Testing (MBT 2007), Braga, Portugal, March 31 - April 1, 2007.
[paper (PDF, 205K)]

Saswat Anand, Corina S. Pasareanu, Willem Visser, "JPF--SE: A Symbolic Execution Extension to Java PathFinder," Proc. TACAS'07: Thirteenth Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Braga, Portugal, Mar. 24- Apr. 1, 2007.
[paper (PDF, 240K)]

Willem Visser, Corina S. Pasareanu, Radek Pelanek, "Test Input Generation for Java Containers using State Matching," Proc. ISSTA'06: Int'l Symposium on Software Testing and Analysis, Portland, Maine, Jul. 18-20, 2006.
[paper (PDF, 150K)]

Willem Visser, Corina S. Pasareanu, Radek Pelanek, "Test Input Generation for Red Black Trees using Abstraction," Proc. ASE'05: 20th IEEE/ACM Int'l Conf. on Automated Engineering, Long Beach, CA, pp. 414-417, Nov. 7-11, 2005.

Willem Visser, Corina S. Pasareanu, Radek Pelanek, "Test Input Generation for Red Black Trees using Abstraction," Proc. ASE'05: 20th IEEE/ACM Int'l Conf. on Automated Engineering, Long Beach, CA, pp. 414-417, Nov. 7-11, 2005.
[paper (PDF, 72K)]

Sarfraz Khurshid, Corina Pasareanu, Willem Visser, "Generalized Symbolic Execution for Model Checking and Testing," Proc. TACAS 2003: 9th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer LNCS, vol. 2619, Warsaw, Poland, pp. 553-568, Apr. 7-11, 2003.
[paper ( PDF, 293K)]

Back to Top

Theorem Proving

David Aspinall, Ewen Denney, and Christoph Lüth, "Tactics for Hierarchical Proof". In Mathematics in Computer Science: Special Issue on Authoring, Digitalization and Management of Mathematical Knowledge, Vol. 3, No. 3, May 2010, p 309-330.
[paper (PDF, 344K)]

Ewen Denney, Nurlida Basir, Bernd Fischer, "Deriving safety cases from automatically constructed proofs" 4th IET International Conference on System Safety, London, UK, Oct. 26 2009.
[paper (link coming...)]

David Aspinall, Ewen Denney, and Christoph Lüth, "A Tactic Language for Hiproofs". In Proc. MKM'08: 7th International Conference on Mathematical Knowledge Management. Birmingham, England, Jul. 28-30 2008.
[paper (PDF, 284K)]

Gilles Dowek, Cesar Munoz, Corina Pasareanu, "A Formal Analysis Framework for PLEXIL," Proc. ICAPS'07: Workshop on Planning and Plan Execution for Real-World Systems, Providence, RI, Sept. 22-26, 2007.
[paper (PDF, 104K)]

Grigore Rosu, Jonathan Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code," Proc. VCL'02: Verification and Computational Logic, Pittsburgh, PA., pp. 29-38, Oct. 5, 2002.
[papers ( PDF, 104K)]

Ewen Denney, Bernd Fischer, "Explaining Verification Conditions," Proc. Formal Methods 2006 , Hamilton, Ontario, Canada, Aug 21-27, 2006.
[paper (PDF, 597K)]

Ewen Denney, John Power, Konstantinos Tourlas, "Hierarchical Proof Structures," Proc. Proceedings of the ICALP Workshop on Structures and Deductions,, Lisbon, Jul 16-17, 2005.
[paper (PDF, 157K)]

Ewen Denney, John Power, Konstantinos Tourlas, "Hiproofs: A hierarchical notion of proof tree," Proc. Mathematical foundations, Burmingham, England, Jun. 10, 2005.
[paper (PDF, 237K)]

Grigore Rosu, Jonathan Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code-Extended Abstract-," Proc. ASE'02: 17th IEEE Int'l Conf. on Automated Software Engineering, Edinburgh, UK, pp. 289-294, Sep. 23-27, 2002.
[papers ( PDF, 79K)]

Klaus Havelund, "Mechanical Verification of a Garbage Collector," Proc. FMPPTA'99: 4th Int'l Workshop on Formal Methods for Parallel Programming: Theory and Applications, San Juan, Puerto Rico, pp. 99-124, Apr. 12-16, 1999.
[tech reports ( PDF, 418K)]
[papers ( PDF, 95K)]

Back to Top

Advanced Validation Testing

Greg Gay, T. Menzies, Misty Davies, and Karen Gundy-Burlet, "How to Automatically Find the Control Variables for Complex System Behavior," Automated Software Engineering Dec. 2010.
[paper (link coming...)]

Misty Davies, Greg Limes, and Karen Gundy-Burlet, "A Hardware Model Validation Tool for Use in Complex Systems," AIAA SPACE 2010 Conference & Exposition (AIAA '10), Anaheim, California, Aug 31-Sep 2, 2010.
[paper (link coming...)]

Sarah Thompson and Misty Davies, "Hybrid Decompositional Verification for Discovering Failures in Adaptive Flight Control Systems,” Infotech@Aerospace (I@A '10), Atlanta, Georgia, Apr 20 - 22, 2010.
[paper (link coming...)]

Misty Davies, Karen Gundy-Burlet, "Visualization of Global Sensitivity Analysis Results Based on a Combination of Linearly Dependent and Independent Directions" Infotech@Aerospace (I@A '10), , Atlanta, GA, Apr 20-22, 2010.
[paper (link coming)]

Back to Top

Miscellaneous

Danny Thomas, Alexia Joiner, Wei Lin, Michael Lowry, Tom Pressburger, "The Unique Aspects of Simulation Verification and Validation," Proc. 2010 IEEE Aerospace Conference, Big Sky, MT, March 6-13, 2010.
[paper (PDF, 147K)]

Karen Gundy-Burlet, Johann Schumann, Tim Menzies, and Tony Barrett, "Parametric Analysis of Antares Re-Entry Guidance Algorithms using Advanced Test Generation and Data Analysis," Proc. i-SAIRAS'08: 9th International Symposium on Artificial Intelligence, Robotics, and Automation in Space , Universal City, California, February 25-29, 2008.
[paper (PDF, 451K)]

Guillaume Brat, "Software Verification for Space Applications Part II: Autonomous Systems," Proc. Universite Catholique De Vouvain Graduate Seminar (Moves), Namur, Belgium, Jun 12, 2007.
[paper (PDF, 620K)]

Julian Richardson, Dan Port, Martin S. Feather, "Deriving Verification and Validation Strategies," Proc. 2007 IEEE Aerospace Conference, Big Sky, MT, Mar. 3-10, 2007

Julian Richardson, Barry Boehm, Ray Madachy, LiGuo Huang, Dan Port, Rick Kazman, "Reducing Autonomy Risks through Rational Selection of Verification Strategies," 2006 Ground Systems Architecture Workshop, Los Angeles, CA, Mar. 27-29, 2006.

Guillaume Brat, Ewen Denney, Dimitra Giannakopoulou, Ari Jonsson, "Verification of Autonomous Systems for Space Applications," 2006 IEEE Aerospace Conference, Big Sky, MT, Mar. 4-11, 2006.
[paper (PDF, 312K)]

Guillaume Brat,Ewen Denney, Kim Farell, Dimitra Giannakopoulou, Ari Jonsson, Jeremy Frank, Mark Boddy,Todd Carpenter, Tara Estlin, "A Robust Compositional Architecture for Autonomous Systems," 2006 IEEE Aerospace Conference, Big Sky, MT, Mar. 4-11, 2006.
[paper (PDF, 400K)]

Owen O' Malley, Masoud Mansouri-Samani, Peter Mehlitz, John Penix, "Seeing the Invisible: Embedding Tests in Code That Cannot be Modified," Proc. AIAA'05 Infotech at Aerospace, Arlington, VA, Sep. 26-28, 2005.
[paper (PDF, 54K)]

Guillaume Brat, Ari Jonsson, "Challenges in verification and validation of autonomous systems for space exploration," Proc. IJCNN'05:Performance of Neuro-Adaptive and Learning Systems: Assessment, Monitoring, and Validation, Montreal, Canada, July 31 - August 4, 2005.
[paper (PDF, 152K)]

Peter Mehlitz, John Penix, "Design for Verification with Dynamic Assertions," Proc. 29th NASA/IEEE Software Engineering Workshop, Greenbelt, MD, pp. 285-292, April 6-7, 2005.

Peter Mehlitz, John Penix, "Design for Verification - Using Design Patterns to Build Reliable Systems," Proc. 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction, Portland, OR, May 3-4, 2003.
[paper (PDF, 121K)]

Klaus Havelund, Scott Stoller, Shmuel Ur, "Benchmark and Framework for Encouraging Research on Multi-Threaded Testing Tools," Proc. PADTAD'03: Parallel and Distributed Systems: Testing and Debugging, Nice, France, pp. 286-294, Apr. 22-26, 2003. (Shmuel Ur was the invited speaker).
[paper ( PDF, 44K)]

Anthony Gross, K.R. Sridhar, William Larson, Daniel Clancy, Charles Pecheur, Geoffrey Briggs, "Information Technology and Control Needs for In-Situ Resource Utilization," Proc. IAF99: 50th Int'l Astronautical Federation Congress, Amsterdam, The Netherlands, Oct. 4-8, 1999.
[papers ( PDF, 791K)]

Michael Lowry, Mark Boyd and Deepak Kulkari, "Towards a Theory for Integration of Mathematical Verification and Empirical Testing," Proc. ICSE'98: 13th IEEE Int'l Conf. on Software Engineering, Los Alamitos, CA., pp. 322-331, Oct. 13-16, 1998.
[paper ( PDF, 1.9M)]

Back to Top

Last modified: In Progress 1 April 2012 by Guy Power.