Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




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

URL of the conference:

http://www.lpar-18.info/

URL for downloading the paper:

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section