Parameter Synthesis with IC3 (Informal Presentation)

Authors Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta

Thumbnail PDF


  • Filesize: 258 kB
  • 2 pages

Document Identifiers

Author Details

Alessandro Cimatti
Alberto Griggio
Sergio Mover
Stefano Tonetta

Cite AsGet BibTex

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter Synthesis with IC3 (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 106-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Parametric systems arise in many application domains, from real-time systems to software to cyber-physical systems. Parameters are fundamental to model unknown quantities at design time and allow a designer to explore different instantiation of the system (i.e. every parameter valuation induces a different system), during the early development phases. A key challenge is to automatically synthesize all the parameter valuations for which the system satisfies some properties. In this talk we focus on the parameter synthesis problem for infinite-state transition systems and invariant properties. We describe the synthesis algorithm Param IC3, which is based on IC3, one of the major recent breakthroughs in SAT-based model checking, and lately extended to the SMT case. The algorithm follows a general approach that first builds the set of "bad" parameter valuations and then obtain the set of "good" valuations by complement. The approach enumerates the counterexamples that violate the property, extracting from each counterexample a region of bad parameter valuations, existentially quantifying the state variables. ParamIC3 follows the same principles, but it overcomes some limitations of the previous approach by exploiting the IC3 features. First, IC3 may find a set of counterexamples s_o, ..., s_k, where each state in s_i is guaranteed to reach some of the bad states in s_k in k-i steps; this is exploited to apply the expensive quantifier elimination on shortest, and thus more amenable, counterexamples. Second, the internal structure of IC3 allows our extension to be integrated in a fully incremental fashion, never restarting the search from scratch to find a new counterexample. While various approaches already solve the parameter synthesis problem for several kind of systems, like infinite-state transition systems, timed and hybrid automata, the advantages ParamIC3 are that: it synthesizes an optimal region of parameters, it avoids computing the whole set of the reachable states, it is incremental and applies quantifier elimination only to small formulas. We present the results of an experimental evaluation performed on benchmarks from the timed and hybrid systems domain. We compared the approach with similar SMT-based techniques and with techniques based on the computation of the reachable states. The results show the potential of our approach.
  • Parameter Synthesis
  • Infinite-state Transition Systems
  • Satisfiability Modulo Theories
  • IC3


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter synthesis with IC3. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 165-168, 2013. Google Scholar