77 citations · 96 across the 8 of their papers we have counts for
5 papers · 1 filter
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…
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,…