TY - GEN
T1 - Validity-guided synthesis of reactive systems from assume-guarantee contracts
AU - Katis, Andreas
AU - Fedyukovich, Grigory
AU - Guo, Huajun
AU - Gacek, Andrew
AU - Backes, John
AU - Gurfinkel, Arie
AU - Whalen, Michael W.
N1 - Publisher Copyright:
© The Author(s) 2018.
Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - 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 reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of ∀ ∃ -formulas. In spirit of IC3/PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKind’s already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.
AB - 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 reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of ∀ ∃ -formulas. In spirit of IC3/PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKind’s already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.
UR - http://www.scopus.com/inward/record.url?scp=85045830043&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85045830043&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-89963-3_10
DO - 10.1007/978-3-319-89963-3_10
M3 - Conference contribution
AN - SCOPUS:85045830043
SN - 9783319899626
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 176
EP - 193
BT - Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
A2 - Beyer, Dirk
A2 - Huisman, Marieke
PB - Springer- Verlag
T2 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Y2 - 14 April 2018 through 20 April 2018
ER -