77 citations · 96 across the 8 of their papers we have counts for
9 papers
Verified Foundations for Differential Privacy
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint +7
Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifyi…
Unlocking the Power of Environment Assumptions for Unit Proofs
Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel
Clearly articulating the assumptions of the execution environment is crucial for the successful application of code-level formal verification. The process of specifying a model for…
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
Geoffrey W. Hamilton, Temesghen Kahsai, Maurizio Proietti
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Prog…
Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis
Temesghen Kahsai, German Vidal
Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around…
Hierarchical State Machines as Modular Horn Clauses
Pierre-Loïc Garoche, Temesghen Kahsai, Xavier Thirioux
In model based development, embedded systems are modeled using a mix of dataflow formalism, that capture the flow of computation, and hierarchical state machines, that capture the…
Verifying the Safety of a Flight-Critical System
Guillaume Brat, David Bushnell, Misty Davies +3
This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercia…
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characte…
Invariant stream generators using automatic abstract transformers based on a decidable logic
Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
The use of formal analysis tools on models or source code often requires the availability of auxiliary invariants about the studied system. Abstract interpretation is currently one…
PKind: A parallel k-induction based model checker
Temesghen Kahsai, Cesare Tinelli
PKind is a novel parallel k-induction-based model checker of invariant properties for finite- or infinite-state Lustre programs. Its architecture, which is strictly message-based,…