17 citations · 28 across the 18 of their papers we have counts for
5 papers · 1 filter
Inductive Predicate Synthesis Modulo Programs (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the…
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existin…
Verifying Verified Code
Siddharth Priya, Xiang Zhou, Yusen Su +3
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explo…
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…
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…