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 | Download | |
|---|---|---|---|---|
| CodeHawk:A High Precision Static Code Analyzer for Detecting Cybersecurity Vulnerabilities | A CodeHawk overview. | NA |  |
|
| Failsafe Project Software Health Management | An overview of the Failsafe project goals and technology. | Barry | |
|
| A Tutorial on Abstract Interpretation as the Theoretical Foundation of CodeHawk&trade | A self-guided presentation to illustrate how abstract interpretaton works | Venet | |
|
| 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 | |
|
| Efficient Strongly Relational Polyhedral Analysis | A method to generate polyhedral invariants with polynomial complexity | Sankaranarayanan, Colon, Sipma, Manna |
|
|
| 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 |
|
|
| Scalable Analysis of Linear Systems using Mathematical Programming | A method that uses linear programming to generate linear invariants with arbitrary coefficients | Sankaranarayanan, Sipma, Manna | |
|
| 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 | |
|
| Precise and Scalable Static Program Analysis of NASA Flight Software | System description and application results on large programs | Brat, Venet | |
|
| 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 |
|
|
| Non-Linear Loop Invariant Generation | A method to generate non-linear (algebraic) invariants using Grobner bases | Sankaranarayanan, Sipma, Manna |
|
|
| Precise and Efficient Static Array Bound Checking for Large Embedded C Programs | Static array bound checker for Mars mission flight control software | Brat, Venet | |
|
| A Scalable Nonuniform Pointer Analysis for Embedded Programs | Efficient yet precise algorithm for handling multithreaded programs | Venet | |
|
| 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 | |
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 | |
| Program Monitoring with LTL in Eagle | Rule-based framework for defining and implementing finite trace monitoring logics | Havelund, Goldberg, Barringer, Sen | |
|
| Petri Net Analysis Using Invariant Generation | A constraint-based method to generate linear invariants for Petri Nets | Sankaranarayanan, Sipma, Manna |
|
|
| 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 |
|
|
| Efficient Monitoring of Safety Properties | Flexible framework for efficient monitoring and analysis of program execution | Havelund, Rosu | |
|
| 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 | |
|
| 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 | |
|
| Verification Diagrams: Logic + Automata | Automata labeled with predicates as temporal abstractions of systems | Manna, Sipma |
|
|
| 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 | |
|
| Reasoning About Actions for Spacecraft Redundancy Management | An application of action description languages to spacecraft operational redundancy problems | Barry, Watson | |
|
| Visual Abstractions for Temporal Verification | Verification diagrams as temporal abstractions of systems | Browne, Manna, Sipma, Uribe |
|