33 citations · 49 across the 11 of their papers we have counts for
5 papers · 1 filter
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…
On Implementing Real-time Specification Patterns Using Observers
John D. Backes, Michael W. Whalen, Andrew Gacek +1
English language requirements are often used to specify the behavior of complex cyber-physical systems. The process of transforming these requirements to a formal specification lan…
Reasoning about Algebraic Data Types with Abstractions
Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen
Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network appl…
Efficient Generation of Inductive Validity Cores for Safety Properties
Elaheh Ghassabani, Andrew Gacek, Michael W. Whalen
Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not generally provide much i…
Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report
Andreas Katis, Michael W. Whalen, Andrew Gacek
In previous work, we have introduced a contract-based real- izability checking algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real ari…