License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.30
URN: urn:nbn:de:0030-drops-128429
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12842/
Go to the corresponding LIPIcs Volume Portal

Ranzato, Francesco

Decidability and Synthesis of Abstract Inductive Invariants

pdf-format:
LIPIcs-CONCUR-2020-30.pdf (0.6 MB)

Abstract

Decidability and synthesis of inductive invariants ranging in a given domain play an important role in software verification. We consider here inductive invariants belonging to an abstract domain A as defined in abstract interpretation, namely, ensuring the existence of the best approximation in A of any system property. In this setting, we study the decidability of the existence of abstract inductive invariants in A of transition systems and their corresponding algorithmic synthesis. Our model relies on some general results which relate the existence of abstract inductive invariants with least fixed points of best correct approximations in A of the transfer functions of transition systems and their completeness properties. This approach allows us to derive decidability and synthesis results for abstract inductive invariants which are applied to the well-known Karr’s numerical abstract domain of affine equalities. Moreover, we show that a recent general algorithm for synthesizing inductive invariants in domains of logical formulae can be systematically derived from our results and generalized to a range of algorithms for computing abstract inductive invariants.

BibTeX - Entry

@InProceedings{ranzato:LIPIcs:2020:12842,
  author =	{Francesco Ranzato},
  title =	{{Decidability and Synthesis of Abstract Inductive Invariants}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12842},
  URN =		{urn:nbn:de:0030-drops-128429},
  doi =		{10.4230/LIPIcs.CONCUR.2020.30},
  annote =	{Keywords: Inductive invariant, program verification, abstract interpretation}
}

Keywords: Inductive invariant, program verification, abstract interpretation
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI