Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover
 
conference paper

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Kovacs, Laura
•
Voronkov, Andrei
2009
Fundamental Approaches To Software Engineering, Proceedings
12th International Conference on Fundamental Applroaches to Software Engineering held in Conjuction with European Conference on Theroy and Practice of Software

We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on the automatic analysis of the so-called update predicates of loops. An update predicate for an array A expresses updates made to A. We observe that many properties of update predicates can be extracted automatically from the loop description and loop properties obtained by other methods such as a simple analysis of counters occurring in the loop, recurrence solving and quantifier elimination over loop variables. We run the theorem prover Vampire on some examples and show that non-trivial loop invariants can be generated.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-00593-0_33
Web of Science ID

WOS:000265405500033

Author(s)
Kovacs, Laura
Voronkov, Andrei
Date Issued

2009

Publisher

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa

Published in
Fundamental Approaches To Software Engineering, Proceedings
ISBN of the book

978-3-642-00592-3

Series title/Series vol.

Lecture Notes In Computer Science; 5503

Start page

470

End page

485

Subjects

System Description

•

Verification

•

Generation

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
MTC  
Event nameEvent placeEvent date
12th International Conference on Fundamental Applroaches to Software Engineering held in Conjuction with European Conference on Theroy and Practice of Software

York, ENGLAND

Mar 22-29, 2009

Available on Infoscience
November 30, 2010
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/60314
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés