The following papers have been published by KT employees either prior to or during their work at KT. The former are included where they are relevant to KT's mission.

Title Description Author Date Download
SAMATE Case Analysis Report An application of CodeHawk to a NIST benchmark suite. Sipma 2008 Download
Failsafe Project Software Health Management An overview of the Failsafe project goals and technology. Barry 2008 Download
A Tutorial on Abstract Interpretation as the Theoretical Foundation of CodeHawk&trade A self-guided presentation to illustrate how abstract interpretaton works Venet 2007
Towards the Industrial Scale Development of Custom Static Analyzers Use of abstract interpretation to achieve high assurance for security and safety Anton, Bush, Goldberg, Havelund, Smith, Venet 2006
Efficient Strongly Relational Polyhedral Analysis A method to generate polyhedral invariants with polynomial complexity Sankaranarayanan, Colon, Sipma, Manna 2006
Linear Ranking with Reachability A constraint-based method to generate linear ranking functions with supporting linear invariants to prove termination of loops Bradley, Sipma, Manna 2005
Scalable Analysis of Linear Systems using Mathematical Programming A method that uses linear programming to generate linear invariants with arbitrary coefficients Sankaranarayanan, Sipma, Manna 2005
Event-Based Runtime Verification of Java Programs Monitoring is achieved on a state-by-state basis avoiding any need to store the input trace d'Amorim, Havelund 2005
Precise and Scalable Static Program Analysis of NASA Flight Software System description and application results on large programs Brat, Venet 2005
Constraint-based Linear Relations Analysis A constraint-based method to generate linear invariants with efficient heuristics to solve the resulting nonlinear constraint systems Sankaranarayanan, Sipma, Manna 2004
Non-Linear Loop Invariant Generation A method to generate non-linear (algebraic) invariants using Grobner bases Sankaranarayanan, Sipma, Manna 2004
Precise and Efficient Static Array Bound Checking for Large Embedded C Programs Static array bound checker for Mars mission flight control software Brat, Venet 2004
A Scalable Nonuniform Pointer Analysis for Embedded Programs Efficient yet precise algorithm for handling multithreaded programs Venet 2004
Automated Envisioning for Spacecraft Contingencies Mission controllers frequently imagine scenarios in which certain faults have occurred to see how it affects the mission. We present here the advisor system that automates envisioning. Alsaç, Barry 2004
High-level Data Races Investigates data races on a higher abstraction layer to detect inconsistent uses of shared variables, even if no classical race condition occurs Artho, Havelund, Biere 2004
Program Monitoring with LTL in Eagle Rule-based framework for defining and implementing finite trace monitoring logics Havelund, Goldberg, Barringer, Sen 2004
Petri Net Analysis Using Invariant Generation A constraint-based method to generate linear invariants for Petri Nets Sankaranarayanan, Sipma, Manna 2003
Linear Invariant Generation using Non-linear Constraint Solving A method to reduce the generation of linear invariant to solving a non-linear constraint system Colon, Sankaranarayanan, Sipma 2003
Efficient Monitoring of Safety Properties Flexible framework for efficient monitoring and analysis of program execution Havelund, Rosu 2003
Goal Specification Using Temporal Logic in Presence of Non-deterministic Actions Certain goals in the presence of non-deterministic actions can be expressed in LTL and CTL Barel, Barry 2003
An Overview of the Runtime Verification Tool Java PathExplorer Overview of the Java PathExplorer (JPaX) runtime verification tool for monitoring the execution of a Java program to check that it conforms with a set of user provided properties formulated in temporal logic Havelund, Rosu 2003
Verification Diagrams: Logic + Automata Automata labeled with predicates as temporal abstractions of systems Manna, Sipma 2000
An A-Prolog Decision Support System for the Space Shuttle Successful test of declarative programming for knowledge-intensive control of spacecraft functions Nogueira, Balduccini, Gelfond, Watson, Barry 2000
Reasoning About Actions for Spacecraft Redundancy Management An application of action description languages to spacecraft operational redundancy problems Barry, Watson 1999
Visual Abstractions for Temporal Verification Verification diagrams as temporal abstractions of systems Browne, Manna, Sipma, Uribe 1998