Laboratory for Reliable Software (LaRS)
at the Jet Propulsion Laboratory
Cobra: a light-weight tool for static and dynamic analysis, Innovations in Systems and Software Engineering, a NASA Journal, DOI 10.1007/s11334-016-0282-x, pp. 1-15.
Cloud-based Verification of Concurrent Software, Proc. VMCAI 2016, Springer-Verlag, LNCS, Jan. 2016.
Tiny Tools, IEEE Software, Jan/Feb. 2016, pp. 24-28.
K: a Wide Spectrum Language for Modeling, Programming, and Analysis, Proc. ModelsWard 2016, 4th Int. Conf. on Model-Driven Engineering, and Software Development, Feb. 2016, Rome, Italy.
Some recent advances in automated analysis, Springer-Verlag, STTT 18:2, pp. 121-128.
Code Clarity, IEEE Software, Mar/Apr. 2016, pp. 22-25.
Frequently Unanswered Questions, IEEE Software, May/June 2016, pp. 10-12.
The Weakest Link, IEEE Software, July/Aug. 2016, pp. 12-15.
Cobra: a lightweight tool for static and dynamic program analysis, Innovations in Systems and Software Engineering, May 2016, DOI 10.1007/s11334-016-0282-x, pp. 1-15.
Brace Yourself, IEEE Software, Sep/Oct. 2016, pp. 12-15.
Verified Change, Trans. on Foundations for Mastering Change, (to appear).
NFER -- a Notation and System for Inferring Event Stream Abstractions, Proc. 16th Int. Conf. on Runtime Verification, Sept. 2016.
Towards a Unified View of Modeling and Programming, Proc. 7th Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA?16), Oct. 2016.
Towards a Logic for Inferring Properties of Event Streams, Proc. 7th Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA?16), Oct. 2016.
To Code is Human, IEEE Software, Jan/Feb. 2015, pp. 16-19.
Rule-based runtime verification revisted,
Int. Journal on Software Tools for Technology Transfer (STTT), Int. Journal on Software Tools for Technology Transfer, 17:2, pp. 143-170, March 2015.
Code Inflation, IEEE Software, March/April 2015, pp. 10-13.
Domain-Specific Languages with Scala, 17th Int. Conf. on Formal Engineering Methods, Nov. 2015, Springer-Verlag, LNCS, Vol. 9407, pp. 1-16.
Proc. 7th NASA Formal Methods Symposium, April 2015, Springer Verlag, LNCS Vol. 9058.
Assertive Testing, IEEE Software, May/June 2015, pp. 12-15.
Points of Truth, IEEE Software, July/Aug 2015.
A multi-paradigm language for reactive synthesis, Proc. 4th Workshop on Synthesis, July 2015, San Francisco, CA.
Specification of Parametric Monitors -- Quantified Event Automata versus Rule Systems, To appear in Springer Verlag, Lecture Notes in Computer Science, LNCS, pp. 151-189.
Combining Modeling and Programming? Towards Advanced Languages for Software Development, White paper (not published).
Code Evasion, IEEE Software, Sep/Oct. 2015, pp. 77-80.
Out of Bounds, IEEE Software, Nov/Dec. 2015, pp. 24-26.
Communications of the ACM, February 2014, Vol. 57, No. 2, pp. 64-73. (Cover article, 100,000 downloads to date).
An improvement of the piggyback algorithm for parallel model checking,
Proc. Int. Spin Symposium on Model Checking Software, July 2014, ACM Press, pp. 48-57.
Verification and validation meets planning and scheduling,
Int. Journal on Software Tools for Technology Transfer (STTT), Feb. 2014, Vol. 16, No. 1, pp. 1-12.
40 Years of formal methods,
Proc. Formal Methods 2014, Singapore. Springer, Lecture Notes in Computer Science, Vol. 8442, pp. 42-61.
Monitoring with Data Automata,
Proc. 6th Int. Symp. on Leveraging Applications of Formal Methods, Verification and Validation, Oct. 8-11, 2014, Greece, Springer Verlag, LNCS Vol. 8803, pp. 254-273.
Comprehension of spacecraft telemetry using hierarchical specifications of behavior,
Proc. 16th Int. Conf. on Formal Engineering Methods, Nov. 2014, Luxemburg. Springer Verlag, LNCS Vol. 8829, pp. 187-202.
Data Automata in Scala,
8th Int. Symp. on Theoretical Aspects of Software Engineering. Sept. 2014, Changsha, China. IEEE Computer Society Press (invited)
6th Int. Symp. On Leveraging Applications of Formal Methods, Verification and Validation, Oct. 2014, Corfu, Greece. Part I, LNCS 8802, Springer-Verlag.
Experience with Rule-Based Analysis of Spacecraft Logs, 3rd Int. Workshop on Formal Techniques for Safety-Critical Systems. Nov. 2014, Luxembourg, Comm. in Computer and Information Science (CCIS), Springer-Verlag.
Fault Intolerance, IEEE Software, Nov/Dec. 2014, pp. 16-20.
Establishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, and Monitoring,
Annals of Mathematics and Artificial Int., 2014, Vol. 70, No. 4, pp. 315-349.
Landing a Spacecraft on Mars
IEEE Software, Impact Column, March/April 2013, pp. 17-20.
Proving Properties of Concurrent Programs (extended abstract)
Proc. First Spin Symposium, State Univ. of New York at Stony Brook. Springer Verlag, Lecture Notes in Computer Science, Vol. 7976, pp. 18-23.
A Three-Step Program for Recovering Hackers
IEEE Computer, Software Technology Column, June 2013, pp.10-12.
A Tutorial on Runtime Verification Book chapter for:
Summer School Marktoberdorf - Engineering Dependable Software Systems. (held July 31 to August 12, 2012) Eds: Manfred Broy and Doron Peled. IOS Press, 2013.
A Scala DSL for Rete-Based Runtime Verification Proc. 4th Int. Conf. on Runtime Verification, RV 2013, pp. 322-327.
Parallelizing the SPIN model checker
Proc. 19th Int. SPIN Workshop, Oxford, UK, July 2012.
Logic model checking of time-periodic real-time systems,
Proc. Infotech@Aerospace Conference, AIAA, Garden Grove, CA, June 2012 (invited).
Quantified Event Automata - Towards Expressive and Efficient Runtime Monitors,
Proc. Formal Methods (FM 2012), Paris, France.
Requirements-Driven Log Analysis (extended abstract)
Proc. ICTSS 2012, In B. Nielsen and C. Weise, editors, 24th IFIP WG 6.1 Int. Conf. on Testing Software and Systems. held 19-21 Nov. 2012, Aalborg, Denmark. LNCS 7641, Springer-Verlag (invited).
What does AI have to do with RV? (extended abstract)
Proc. ISoLA 2012, In T. Margaria and B. Steffen, editors, 5th Int. Symp. On Leveraging Applications of Formal Methods, Verification and Validation. Track: Runtime Verification. held 15-18 Oct. 2012, Heraclion, Crete. LNCS 7610, Springer-Verlag (invited).
Reliable software development: analysis aware design
Proc. European Joint Conferences on Theory and Practice of Software (ETAPS), keynote, Saarbrucken, Germany, April 2011.
Software Certification - Coding, Code, and Coders, Proc. Int. Conf. on Embedded Software, EMSOFT 2011, Oct., Taipei, Taiwain. (invited).
Swarm Verification Techniques,
IEEE Trans. on Software Engineering, Vol. 37, No. 6, Nov/Dec. 2011, pp. 845-857.
Model checking with bounded context switching,
Formal Aspects of Computing, 2011, Vol. 23, Issue 3, pp. 365-389.
Checking Flight Rules with TraceContract: Application of a Scala DSL for Trace Analysis, Proc. Scala Days 2011, June 2-3, 2011.
TraceContract: A Scala DSL for Trace Analysis, Proc. 17th Int. Symposium on Formal Methods, Limerick, Ireland, June 2011, Springer-Verlag, Lecture Notes in Computer Science, Vol. 6664.
Model checking multitask applications for OSEK compliant real-time operating systems,
Proc. 17th IEEE Pacific Rim Int. Symposium on Dependable Computing (PRDC 2011), Pasadena, CA, Dec. 12-14, 2011.
Closing the Gap Between Specification and Programming: VDM++ and Scala,
Proc. Higher-Order Workshop on Automated Runtime Verification and Debugging. December 2011, Manchester, UK (invited).
Implementing Runtime Monitors,
Proc. TORRENTS 2011, 2nd TORRENTS Workshop, December 2011, Toulouse, France (invited).
Aspect-Oriented Instrumentation with GCC,
Proc. 1st Int. Conference on Runtime Verification (RV 2010), St. Julians, Malta, November 1-4, 2010, Springer-Verlag, Lecture Notes in Computer Science, Vol. 6418.
Formal Analysis of Log Files,
Journal of Aerospace Computing, Information, and Communication, Vol. 7, Issue 11, November 2010.
(Invited talk given at the SMC-IT workshop: Software Reliability for Space Missions. July 20, 2009, Pasadena, California, USA)
Prototyping a Domain-Specific Language for Monitor and Control Systems,
Journal of Aerospace Computing, Information, and Communication, Vol. 7, Issue 11, Nov. 2010.
Detection of Deadlock Potentials in Multi-Threaded Programs,
IBM Journal of Research & Development, Vol. 54, Issue 5, September 2010.
Scrub: a tool for code reviews,
Innovations in Systems and Software Engineering, Vol. 6, Nr. 4, 2010, pp. 311-318.
From Scripts to Specifications,
ACM/IEEE 32nd International Conference on Software Engineering (ICSE 2010) Cape Town, South Africa, May 2-8, 2010.
A Case Study in DSL Development - An Experiment with Python and Scala,
Scala Days 2010, April 15-16, 2010, Lausanne, Switzerland.
Aspect-oriented Race Detection in Java,
IEEE Trans. of Software Engineering
(invited journal version of ISSTA'08 paper, Vol. 36, No. 4, pp. 509-527.
Proc. Seventh Int. Workshop on Dynamic Analysis. (WODA), Chicago, July 20, 2009.
Extending model checking with dynamic analysis,
Proc. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI).
San Francisco, California, January 2008, pp. 142-156.
Exploiting traces in static program analysis,
Int. Journal on Software Tools for Technology Transfer (STTT).
Vol. 10, No. 2, pp 131-144, March 2008.
Development of a Prototype Domain-Specific Language for Monitor and Control Systems,
IEEE Aerospace Conference, Big Sky, Montana, March 1-8, 2008.
Aspect-Oriented Monitoring of C Programs,
Sixth IARP-IEEE/RAS-EURON Joint Workshop on Technical Challenges for Dependable Robots in Human Environments,
Pasadena, CA, May 17-18, 2008.
Runtime Verification of C Programs,
The first combined TestCom/FATES conference, Tokyo, Japan, June 10-13, 2008.
Rule Systems for Runtime Verification: A Short Tutorial,
Tutorial presented at RV'09, RV2009, pp. 1-24.
Grenoble, France, June 26-28, 2009.
Proc. 1st Dagstuhl Seminar on Runtime Verification, 2008.
Rule Systems for Run-Time Monitoring: from Eagle to RuleR,
Invited for special issue of the Journal of Logic and Computation (JLC),
(selected papers from 7th Int. Workshop on Runtime Verification).
RACER: Effective race detection using AspectJ,
Int. Symposium on Software Testing and Analysis (ISSTA 2008),
Seattle, WA, July 20-24 2008.
Requirements Capture with RCAT,
Proc. 16th IEEE Int. Requirements Engineering Conference
Barcelona, Spain, Sept. 8-12, 2008.
Verifying multi-threaded C programs with Spin,
Proc. 15th Spin Workshop, UCLA, August 2008.
Tackling large verification problems with Swarms,
Proc. 15th Spin Workshop,
UCLA, August 2008. LNCS 5156.
Random testing and model checking: building a common framework for nondeterministic exploration,
Proc. Sixth International Workshop on Dynamic Analysis, WODA,
Seattle, July 21, 2008.
Random Test Run Length and Effectiveness,
Proc. IEEE/ACM Conference on Automated Software Engineering, (ASE),
L'Aquila, Italy, Sept. 2008.
Automated testing of planning models
Proc. Workshop on Model Checking and Artificial Intelligence,
Patras, Greece, July 2008.
Putting flight software through the paces with testing, model checking, and constraint solving
Proc. Int. Workshop on Constraints in Formal Verification,
Sydney, Australia, August 2008.
Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering,
l'Aquila, Italy, Sept. 2008.
Software Safety and Rocket Science, ECRIM News 75, On Safety-Critical Software, European Research Consortium for Informatics and Mathematics, Oct. 2008.
Model driven code checking,
Automated Software Engineering Journal,
Vol. 15, Nr. 3-4, Dec. 2008, pp. 283-297.
Multi-core model checking with Spin
Proc. HIPS-TopModels 2007, Long Beach, March 26-30, 2007.
Rule Systems for Run-time Monitoring: from Eagle to RuleR,
Proc. 7th International Workshop on Runtime Verification.
Affiliated with 6th Int. Conf. on Aspect-Oriented Software Development,
Vancouver, March 2007. To be published in LNCS.
Randomized differential testing as a prelude to formal verification ,
Proc. Int. Conf. on Software Engineering (ICSE 2007).
Minneapolis, Minnesota, May 2007, pp. 621-631.
A stack-slicing algorithm for multi-core model checking
Proc. 6th Int. Workshop on Parallel and Distributed Methods in Verification (PDMC).
Berlin, July 8, 2007, pp. 1-15.
Visualization of concurrent program executions,
Proc. 31sth Annual IEEE Int. Computer Software and Applications Conf. (COMPSAC),
Beijng, China, July 23-27, 2007.
The Design of a multi-core extension of the Spin Model Checker,
IEEE Trans. on Software Engineering,
Vol. 33, No. 10, pp. 659-674, October 2007.
Verifying C++ with STL containers via predicate abstraction
Proc. Conf. on Automated Software Engineering (ASE).
Atlanta, Georgia, Nov. 2007, pp. 521-524.
RAISE in Perspective,
Invited chapter in Logics of Specification Languages.
Edited by Dines Bjorner and Martin Henson.
To be published in the EATCS textbook series of Springer in Late 2007. link
IEEE Computer, December 2007, pp. 102-104.
Exploiting traces in static program analysis,
Proc. 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
Springer Verlag, LNCS 3920, pp. 379-393, Vienna, Austria, March 2006.
Recommended design and development practices to increase software safety,
JPL Report, prepared for NASA Kennedy Space Center, March 24, 2006, 27 pgs.
Explaining abstract counterexamples,
(submitted for publication)
Adaptive Model Checking,
Logic Journal of IGPL, pp. 729-744, Oct. 2006.
Error Explanation with Distance Metrics
Int. Journal on Software Tools for Technology Transfer, Vol. 8, Nr. 3, pp. 229-247, June 2006.
The Power of Ten: Rules for Developing Safety Critical Code,
IEEE Computer, June 2006.
New Challenges in Model Checking,
Proc. Symposium 25 Years of Model Checking, Federated Logic Conference (FLOC), Seattle, August 2006.
Denali: A practical algorithm for generating optimal code,
Trans. on Programming Languages and Systems (TOPLAS),
Vol. 22, Issue 6, Nov. 2006, pp. 967-989.
The Design of a multi-core extension of the Spin Model Checker,
presented at Formal Methods in Computer Aided Design (FMCAD), San Jose, November 2006.
Model checking artificial intelligence based planners,
Proc. 2005 Aerospace Conf., IEEE, Big Sky MT USA, March 2005.
Software model checking with Spin,
in: Advances in Computers, Vol. 65, Ed. M. Zelkowitz,
Elsevier Publ., Amsterdam, pp.77-108, July 2005.
Theorem proving with lazy proof explication,
Proc. Computer-Aided Verification (CAV),
Boulder, CO, July 2003.
Improving Spin's partial-order reduction for breadth-first search,
Proc. 12th Int. Spin Workshop, San Francisco, August 2005, Springer Verlag, LNCS 3639, pp. 91-105.
Reliable software systems design: defect prevention, detection, and containment
Proc. Verified Software -- Theories, Tools, Experiments, Zurich, October 2005, Springer Verlag, LNCS 4171, pp. 237-244.
A mini grand challenge: build a verifiable filesystem
Proc. Verified Software -- Theories, Tools, Experiments, Zurich, October 2005, Springer Verlag, LNCS 4171, pp. 49-56.
Model-driven software verification,
Proc. 11th Spin Workshop, Barcelona, Spain, April 2004,
Springer Verlag, LNCS 2989, pp. 77-92.
Trends in software verification,
Proc. FM 2003, Formal Methods Europe, Pisa, Italy, Sept. 2003,
Springer Verlag, LNCS 2805, pp. 40-50,
Checking cache coherence protocols with TLA+,
Formal Methods in System Design,
Vol. 22, Nr. 2, Mar. 2003, pp. 125-131.
Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking,
Software Tools for Technology Transfer, 2003, Vol. 4, No. 4, pp. 505-528.
Contact InformationKlaus Havelund / Rajeev Joshi
4800 Oak Grove Dr.
Pasadena, CA 91109-8099
E-mail: Firstname dot Lastname at JPL dot NASA dot gov
Employment OpportunitiesApplications for positions in LaRS are welcome. Please send an e-mail with a statement of interest and a resume. We specifically seek candidates with a strong background in formal methods and software verification techniques. To be eligible for employment by JPL, candidates must be US citizens or have permanent residence in the U.S.
We also welcome applications for long- or short-term internships. Please check with us if you are interested.