MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Fietzke, Arnaud
Kruglov, Evgeny
Weidenbach, Christoph
dblp
dblp
dblp
Editor(s):
Bjørner, Nikolaj
Voronkov, Andrei
dblp
dblp
Not MPII Editor(s):
Bjørner, Nikolaj
Voronkov, Andrei
BibTeX cite key*:
FietzkeKruglovWeidenbach2012
Title, Booktitle
Title*:
Automatic Generation of Invariants for Circular Derivations in SUP(LA)
Booktitle*:
Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18
Event, URLs
Conference URL::
http://www.lpar-18.info/
Downloading URL:
http://dx.doi.org/10.1007/978-3-642-28717-6_17
Event Address*:
Mérida, Venezuela
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
10 March 2012
Event End Date:
15 March 2012
Publisher
Name*:
Springer
URL:
Address*:
Berlin
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
7180
Number:
Month:
Pages:
197-211
Year*:
2012
VG Wort Pages:
ISBN/ISSN:
978-3-642-28716-9
Sequence Number:
DOI:
10.1007/978-3-642-28717-6_17
Note, Abstract, ©
(LaTeX) Abstract:
The hierarchic combination of linear arithmetic and firstorder
logic with free function symbols, FOL(LA), results in a strictly
more expressive logic than its two parts. The SUP(LA) calculus can be
turned into a decision procedure for interesting fragments of FOL(LA).
For example, reachability problems for timed automata can be decided
by SUP(LA) using an appropriate translation into FOL(LA). In this paper,
we extend the SUP(LA) calculus with an additional inference rule,
automatically generating inductive invariants from partial SUP(LA)
derivations. The rule enables decidability of more expressive fragments,
including reachability for timed automata with unbounded integer variables.
We have implemented the rule in the SPASS(LA) theorem prover
with promising results, showing that it can considerably speed up proof
search and enable termination of saturation for practically relevant
problems.
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{FietzkeKruglovWeidenbach2012,
AUTHOR = {Fietzke, Arnaud and Kruglov, Evgeny and Weidenbach, Christoph},
EDITOR = {Bjørner, Nikolaj and Voronkov, Andrei},
TITLE = {Automatic Generation of Invariants for Circular Derivations in {SUP(LA)}},
BOOKTITLE = {Logic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18},
PUBLISHER = {Springer},
YEAR = {2012},
VOLUME = {7180},
PAGES = {197--211},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Mérida, Venezuela},
ISBN = {978-3-642-28716-9},
DOI = {10.1007/978-3-642-28717-6_17},
}


Entry last modified by Anja Becker, 03/07/2013
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
05/11/2012 01:32:52 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Anja Becker
Uwe Brahm
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Edit Dates
07.03.2013 13:32:32
23-01-2013 11:19:08 AM
23.01.2013 11:15:05
15.01.2013 13:42:50
19.12.2012 10:59:40