Synthesizing Modular Invariants for Synchronous Code

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 characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program...

Full description

Bibliographic Details
Main Authors: Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
Format: Article
Language:English
Published: Open Publishing Association 2014-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1412.1152v1