Publications (7)
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
Andreas Katis, Grigory Fedyukovich, Andrew Gacek +3
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizabilit…
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Andreas Katis, Grigory Fedyukovich, Huajun Guo +4
Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of re…
Requirements Analysis of a Quad-Redundant Flight Control System
John Backes, Darren Cofer, Steven Miller +1
In this paper we detail our effort to formalize and prove requirements for the Quad-redundant Flight Control System (QFCS) within NASA's Transport Class Model (TCM). We use a compo…
Towards Realizability Checking of Contracts using Theories
Andrew Gacek, Andreas Katis, Michael W. Whalen +2
Virtual integration techniques focus on building architectural models of systems that can be analyzed early in the design cycle to try to lower cost, reduce risk, and improve quali…
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
Nick Feng, Alan J. Hu, Sam Bayless +5
Generating proofs of unsatisfiability is a valuable capability of most SAT solvers, and is an active area of research for SMT solvers. This paper introduces the first method to eff…
The JKind Model Checker
Andrew Gacek, John Backes, Mike Whalen +2
JKind is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKind uses multiple parallel engines to prove or falsify safety prop…