# The Year Before Last

Ábrahám, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., … Sturm, T. (2016a). Satisfiability Checking and Symbolic Computation.

*ACM Communications in Computer Algebra*,*50*(4). doi:10.1145/3055282.3055285Export

BibTeX

@article{AbrahamCCA2016,
TITLE = {Satisfiability Checking and Symbolic Computation},
AUTHOR = {{\'A}brah{\'a}m, Erika and Abbott, John and Becker, Bernd and Bigatti, Anna M. and Brain, Martin and Buchberger, Bruno and Cimatti, Alessandro and Davenport, James H. and England, Matthew and Fontaine, Pascal and Forrest, Stephen and Griggio, Alberto and Kroening, Daniel and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
DOI = {10.1145/3055282.3055285},
PUBLISHER = {ACM},
ADDRESS = {New York, NY},
YEAR = {2016},
DATE = {2016},
JOURNAL = {ACM Communications in Computer Algebra},
VOLUME = {50},
NUMBER = {4},
PAGES = {145--147},
}

Endnote

%0 Journal Article
%A Ábrahám, Erika
%A Abbott, John
%A Becker, Bernd
%A Bigatti, Anna M.
%A Brain, Martin
%A Buchberger, Bruno
%A Cimatti, Alessandro
%A Davenport, James H.
%A England, Matthew
%A Fontaine, Pascal
%A Forrest, Stephen
%A Griggio, Alberto
%A Kroening, Daniel
%A Seiler, Werner M.
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Satisfiability Checking and Symbolic Computation :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-8ACA-3
%R 10.1145/3055282.3055285
%7 2016
%D 2016
%J ACM Communications in Computer Algebra
%V 50
%N 4
%& 145
%P 145 - 147
%I ACM
%C New York, NY

Ábrahám, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., … Sturm, T. (2016b). Satisfiability Checking and Symbolic Computation. Retrieved from http://arxiv.org/abs/1607.06945

(arXiv: 1607.06945) Abstract

Symbolic Computation and Satisfiability Checking are viewed as individual
research areas, but they share common interests in the development,
implementation and application of decision procedures for arithmetic theories.
Despite these commonalities, the two communities are currently only weakly
connected. We introduce a new project SC-square to build a joint community in
this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the
same name. We aim to strengthen the connection between these communities by
creating common platforms, initiating interaction and exchange, identifying
common challenges, and developing a common roadmap. This abstract and
accompanying poster describes the motivation and aims for the project, and
reports on the first activities.

Export

BibTeX

@online{Sturm1607.06945,
TITLE = {Satisfiability Checking and Symbolic Computation},
AUTHOR = {{\'A}brah{\'a}m, Erika and Abbott, John and Becker, Bernd and Bigatti, Anna M. and Brain, Martin and Buchberger, Bruno and Cimatti, Alessandro and Davenport, James H. and England, Matthew and Fontaine, Pascal and Forrest, Stephen and Griggio, Alberto and Kroening, Daniel and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1607.06945},
EPRINT = {1607.06945},
EPRINTTYPE = {arXiv},
YEAR = {2016},
ABSTRACT = {Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities.},
}

Endnote

%0 Report
%A Ábrahám, Erika
%A Abbott, John
%A Becker, Bernd
%A Bigatti, Anna M.
%A Brain, Martin
%A Buchberger, Bruno
%A Cimatti, Alessandro
%A Davenport, James H.
%A England, Matthew
%A Fontaine, Pascal
%A Forrest, Stephen
%A Griggio, Alberto
%A Kroening, Daniel
%A Seiler, Werner M.
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Satisfiability Checking and Symbolic Computation :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-A959-7
%U http://arxiv.org/abs/1607.06945
%D 2016
%X Symbolic Computation and Satisfiability Checking are viewed as individual
research areas, but they share common interests in the development,
implementation and application of decision procedures for arithmetic theories.
Despite these commonalities, the two communities are currently only weakly
connected. We introduce a new project SC-square to build a joint community in
this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the
same name. We aim to strengthen the connection between these communities by
creating common platforms, initiating interaction and exchange, identifying
common challenges, and developing a common roadmap. This abstract and
accompanying poster describes the motivation and aims for the project, and
reports on the first activities.
%K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO

Ábrahám, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., … Sturm, T. (2016c). SC2: Satisfiability Checking Meets Symbolic Computation. In

*Intelligent Computer Mathematics (CICM 2016)*. Bialystok, Poland: Springer. doi:10.1007/978-3-319-42547-4_3Export

BibTeX

@inproceedings{Abraham_CICM2016,
TITLE = {${SC}^{2}$: {S}atisfiability Checking Meets Symbolic Computation},
AUTHOR = {{\'A}brah{\'a}m, Erika and Abbott, John and Becker, Bernd and Bigatti, Anna M. and Brain, Martin and Buchberger, Bruno and Cimatti, Allesandro and Davenport, James H. and England, Matthew and Fontaine, Pascal and Forrest, Stephen and Griggio, Alberto and Kroening, Daniel and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
ISBN = {978-3-319-42546-7},
DOI = {10.1007/978-3-319-42547-4_3},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Intelligent Computer Mathematics (CICM 2016)},
EDITOR = {Kohlhase, Michael and Johansson, Moa and Miller, Bruce and de Moura, Leonardo and Tompa, Frank},
PAGES = {28--43},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {9791},
ADDRESS = {Bialystok, Poland},
}

Endnote

%0 Conference Proceedings
%A Ábrahám, Erika
%A Abbott, John
%A Becker, Bernd
%A Bigatti, Anna M.
%A Brain, Martin
%A Buchberger, Bruno
%A Cimatti, Allesandro
%A Davenport, James H.
%A England, Matthew
%A Fontaine, Pascal
%A Forrest, Stephen
%A Griggio, Alberto
%A Kroening, Daniel
%A Seiler, Werner M.
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T SC2: Satisfiability Checking Meets Symbolic Computation : Project Paper
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0A83-3
%R 10.1007/978-3-319-42547-4_3
%D 2016
%B 9th International Conference on Intelligent Computer Mathematics
%Z date of event: 2016-07-25 - 2016-07-29
%C Bialystok, Poland
%B Intelligent Computer Mathematics
%E Kohlhase, Michael; Johansson, Moa; Miller, Bruce; de Moura, Leonardo; Tompa, Frank
%P 28 - 43
%I Springer
%@ 978-3-319-42546-7
%B Lecture Notes in Artificial Intelligence
%N 9791

Ábrahám, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., … Sturm, T. (2016d). SC2: Satisfiability Checking meets Symbolic Computation (Project Paper). Retrieved from http://arxiv.org/abs/1607.08028

(arXiv: 1607.08028) Abstract

Symbolic Computation and Satisfiability Checking are two research areas, both
having their individual scientific focus but sharing also common interests in
the development, implementation and application of decision procedures for
arithmetic theories. Despite their commonalities, the two communities are
rather weakly connected. The aim of our newly accepted SC-square project
(H2020-FETOPEN-CSA) is to strengthen the connection between these communities
by creating common platforms, initiating interaction and exchange, identifying
common challenges, and developing a common roadmap from theory along the way to
tools and (industrial) applications. In this paper we report on the aims and on
the first activities of this project, and formalise some relevant challenges
for the unified SC-square community.

Export

BibTeX

@online{Sturm1607.08028,
TITLE = {${SC}^{2}$: {S}atisfiability Checking meets Symbolic Computation (Project Paper)},
AUTHOR = {{\'A}brah{\'a}m, Erika and Abbott, John and Becker, Bernd and Bigatti, Anna M. and Brain, Martin and Buchberger, Bruno and Cimatti, Alessandro and Davenport, James H. and England, Matthew and Fontaine, Pascal and Forrest, Stephen and Griggio, Alberto and Kroening, Daniel and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1607.08028},
EPRINT = {1607.08028},
EPRINTTYPE = {arXiv},
YEAR = {2016},
ABSTRACT = {Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community.},
}

Endnote

%0 Report
%A Ábrahám, Erika
%A Abbott, John
%A Becker, Bernd
%A Bigatti, Anna M.
%A Brain, Martin
%A Buchberger, Bruno
%A Cimatti, Alessandro
%A Davenport, James H.
%A England, Matthew
%A Fontaine, Pascal
%A Forrest, Stephen
%A Griggio, Alberto
%A Kroening, Daniel
%A Seiler, Werner M.
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T SC2: Satisfiability Checking meets Symbolic Computation (Project Paper) :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-A967-7
%U http://arxiv.org/abs/1607.08028
%D 2016
%X Symbolic Computation and Satisfiability Checking are two research areas, both
having their individual scientific focus but sharing also common interests in
the development, implementation and application of decision procedures for
arithmetic theories. Despite their commonalities, the two communities are
rather weakly connected. The aim of our newly accepted SC-square project
(H2020-FETOPEN-CSA) is to strengthen the connection between these communities
by creating common platforms, initiating interaction and exchange, identifying
common challenges, and developing a common roadmap from theory along the way to
tools and (industrial) applications. In this paper we report on the aims and on
the first activities of this project, and formalise some relevant challenges
for the unified SC-square community.
%K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO

Althaus, E., Beber, B., Damm, W., Disch, S., Hagemann, W., Rakow, A., … Wirtz, B. (2016).

*Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization*(No. ATR103). SFB/TR 14 AVACS.Abstract

This paper provides a suite of optimization techniques for
the verification of safety properties of linear hybrid
automata with large discrete state spaces, such as
naturally arising when incorporating health state
monitoring and degradation levels into the controller
design. Such models can -- in contrast to purely functional
controller models -- not analyzed with hybrid verification
engines relying on explicit representations of modes, but
require fully symbolic representations for both the
continuous and discrete part of the state space. The
optimization techniques shown yield consistently a speedup
of about 20 against previously published results for a
similar benchmark suite, and complement these with new
results on counterexample guided abstraction refinement. In
combination with the methods guaranteeing preciseness of
abstractions, this allows to significantly extend the class
of models for which safety can be established, covering in
particular models with 23 continuous variables and 2 to the
71 discrete states, 20 continuous variables and 2 to the
199 discrete states, and 9 continuous variables and 2 to
the 271 discrete states.

Export

BibTeX

@techreport{AlthausBeberDammEtAl2016ATR,
TITLE = {Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization},
AUTHOR = {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner and Disch, Stefan and Hagemann, Willem and Rakow, Astrid and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR103},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2016},
DATE = {2016},
ABSTRACT = {This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.},
TYPE = {AVACS Technical Report},
VOLUME = {103},
}

Endnote

%0 Report
%A Althaus, Ernst
%A Beber, Björn
%A Damm, Werner
%A Disch, Stefan
%A Hagemann, Willem
%A Rakow, Astrid
%A Scholl, Christoph
%A Waldmann, Uwe
%A Wirtz, Boris
%+ Algorithms and Complexity, MPI for Informatics, Max Planck Society
Algorithms and Complexity, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Verification of Linear Hybrid Systems with Large Discrete
State Spaces: Exploring the Design Space for Optimization :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4540-0
%Y SFB/TR 14 AVACS
%D 2016
%P 93 p.
%X This paper provides a suite of optimization techniques for
the verification of safety properties of linear hybrid
automata with large discrete state spaces, such as
naturally arising when incorporating health state
monitoring and degradation levels into the controller
design. Such models can -- in contrast to purely functional
controller models -- not analyzed with hybrid verification
engines relying on explicit representations of modes, but
require fully symbolic representations for both the
continuous and discrete part of the state space. The
optimization techniques shown yield consistently a speedup
of about 20 against previously published results for a
similar benchmark suite, and complement these with new
results on counterexample guided abstraction refinement. In
combination with the methods guaranteeing preciseness of
abstractions, this allows to significantly extend the class
of models for which safety can be established, covering in
particular models with 23 continuous variables and 2 to the
71 discrete states, 20 continuous variables and 2 to the
199 discrete states, and 9 continuous variables and 2 to
the 271 discrete states.
%B AVACS Technical Report
%N 103
%@ false
%U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_103.pdf

Azmy, N. (2016).

*A Machine-checked Proof of Correctness of Pastry*. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291-scidok-67309Abstract

A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key.
Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry.
Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size.
Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols

Export

BibTeX

@phdthesis{Azmyphd16,
TITLE = {A Machine-checked Proof of Correctness of Pastry},
AUTHOR = {Azmy, Noran},
LANGUAGE = {eng},
URL = {urn:nbn:de:bsz:291-scidok-67309},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2016},
DATE = {2016},
ABSTRACT = {A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key. Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry. Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size. Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols},
}

Endnote

%0 Thesis
%A Azmy, Noran
%Y Weidenbach, Christoph
%A referee: Merz, Stephan
%+ Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T A Machine-checked Proof of Correctness of Pastry :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-3BAD-9
%U urn:nbn:de:bsz:291-scidok-67309
%I Universität des Saarlandes
%C Saarbrücken
%D 2016
%P ix, 119 p.
%V phd
%9 phd
%X A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key.
Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry.
Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size.
Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols
%U http://scidok.sulb.uni-saarland.de/volltexte/2017/6730/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

Azmy, N., Merz, S., & Weidenbach, C. (2016). A Rigorous Correctness Proof for Pastry. In

*Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016)*. Linz, Austria: Springer. doi:10.1007/978-3-319-33600-8_5Export

BibTeX

@inproceedings{AzmyABZ2016,
TITLE = {A Rigorous Correctness Proof for {Pastry}},
AUTHOR = {Azmy, Noran and Merz, Stephan and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-33599-5},
DOI = {10.1007/978-3-319-33600-8_5},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016)},
EDITOR = {Butler, Michael and Schewe, Klaus-Dieter and Mashkoor, Atif and Biro, Miklos},
PAGES = {86--101},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {9675},
ADDRESS = {Linz, Austria},
}

Endnote

%0 Conference Proceedings
%A Azmy, Noran
%A Merz, Stephan
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Rigorous Correctness Proof for Pastry :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-01C5-C
%R 10.1007/978-3-319-33600-8_5
%D 2016
%B 5th International ABZ Conference
%Z date of event: 2016-05-23 - 2016-05-27
%C Linz, Austria
%B Abstract State Machines, Alloy, B, TLA, VDM, and Z
%E Butler, Michael; Schewe, Klaus-Dieter; Mashkoor, Atif; Biro, Miklos
%P 86 - 101
%I Springer
%@ 978-3-319-33599-5
%B Lecture Notes in Computer Science
%N 9675

Blanchette, J. C., Fleury, M., & Weidenbach, C. (2016). A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. In

*Automated Reasoning (IJCAR 2016)*. Coimbra, Portugal: Springer. doi:10.1007/978-3-319-40229-1_4Export

BibTeX

@inproceedings{BlanchetteIJCAR2016,
TITLE = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality},
AUTHOR = {Blanchette, Jasmin Christian and Fleury, Mathias and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-40228-4},
DOI = {10.1007/978-3-319-40229-1_4},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Automated Reasoning (IJCAR 2016)},
EDITOR = {Olivetti, Nicola and Tiwari, Ashish},
PAGES = {25--44},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {9706},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Blanchette, Jasmin Christian
%A Fleury, Mathias
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-01C7-8
%R 10.1007/978-3-319-40229-1_4
%D 2016
%B 8th International Joint Conference on Automated Reasoning
%Z date of event: 2016-06-27 - 2016-07-02
%C Coimbra, Portugal
%B Automated Reasoning
%E Olivetti, Nicola; Tiwari, Ashish
%P 25 - 44
%I Springer
%@ 978-3-319-40228-4
%B Lecture Notes in Artificial Intelligence
%N 9706

Blanchette, J. C., Böhme, S., Fleury, M., Smolka, S. J., & Steckermeier, A. (2016). Semi-intelligible Isar Proofs from Machine-Generated Proofs.

*Journal of Automated Reasoning*,*56*(2). doi:10.1007/s10817-015-9335-3Export

BibTeX

@article{BlanchetteJAR2016,
TITLE = {Semi-intelligible {Isar} Proofs from Machine-Generated Proofs},
AUTHOR = {Blanchette, Jasmin Christian and B{\"o}hme, Sascha and Fleury, Mathias and Smolka, Steffen Juilf and Steckermeier, Albert},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-015-9335-3},
PUBLISHER = {Springer},
ADDRESS = {Dordrecht},
YEAR = {2016},
DATE = {2016},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {56},
NUMBER = {2},
PAGES = {155--200},
}

Endnote

%0 Journal Article
%A Blanchette, Jasmin Christian
%A Böhme, Sascha
%A Fleury, Mathias
%A Smolka, Steffen Juilf
%A Steckermeier, Albert
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Semi-intelligible Isar Proofs from Machine-Generated Proofs :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0029-C69A-B
%R 10.1007/s10817-015-9335-3
%7 2015
%D 2016
%J Journal of Automated Reasoning
%V 56
%N 2
%& 155
%P 155 - 200
%I Springer
%C Dordrecht
%@ false

Blanchette, J. C., Greenaway, D., Kaliszyk, C., Kühlwein, D., & Urban, J. (2016). A Learning-Based Fact Selector for Isabelle/HOL.

*Journal of Automated Reasoning*,*57*(3). doi:10.1007/s10817-016-9362-8Export

BibTeX

@article{Blanchette2016JAR,
TITLE = {A Learning-Based Fact Selector for {I}sabelle/{HOL}},
AUTHOR = {Blanchette, Jasmin Christian and Greenaway, David and Kaliszyk, Cezary and K{\"u}hlwein, Daniel and Urban, Josef},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-016-9362-8},
PUBLISHER = {Springer},
ADDRESS = {Dordrecht, Holland},
YEAR = {2016},
DATE = {2016},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {57},
NUMBER = {3},
PAGES = {219--244},
}

Endnote

%0 Journal Article
%A Blanchette, Jasmin Christian
%A Greenaway, David
%A Kaliszyk, Cezary
%A Kühlwein, Daniel
%A Urban, Josef
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
External Organizations
%T A Learning-Based Fact Selector for Isabelle/HOL :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002A-4301-0
%R 10.1007/s10817-016-9362-8
%7 2016
%D 2016
%J Journal of Automated Reasoning
%V 57
%N 3
%& 219
%P 219 - 244
%I Springer
%C Dordrecht, Holland
%@ false

Blanchette, J. C., Böhme, S., Popescu, A., & Smallbone, N. (2016). Encoding Monomorphic and Polymorphic Types. doi:10.2168/LMCS-2014-1018

(arXiv: 1609.08916) Abstract

Many automatic theorem provers are restricted to untyped logics, and existing
translations from typed logics are bulky or unsound. Recent research proposes
monotonicity as a means to remove some clutter when translating monomorphic to
untyped first-order logic. Here we pursue this approach systematically,
analysing formally a variety of encodings that further improve on efficiency
while retaining soundness and completeness. We extend the approach to rank-1
polymorphism and present alternative schemes that lighten the translation of
polymorphic symbols based on the novel notion of "cover". The new encodings are
implemented in Isabelle/HOL as part of the Sledgehammer tool. We include
informal proofs of soundness and correctness, and have formalised the
monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new
encodings vastly superior to previous schemes.

Export

BibTeX

@online{Blanchette1609.08916,
TITLE = {Encoding Monomorphic and Polymorphic Types},
AUTHOR = {Blanchette, Jasmin Christian and B{\"o}hme, Sascha and Popescu, Andrei and Smallbone, Nicholas},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1609.08916},
DOI = {10.2168/LMCS-2014-1018},
EPRINT = {1609.08916},
EPRINTTYPE = {arXiv},
YEAR = {2016},
ABSTRACT = {Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.},
}

Endnote

%0 Report
%A Blanchette, Jasmin Christian
%A Böhme, Sascha
%A Popescu, Andrei
%A Smallbone, Nicholas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
%T Encoding Monomorphic and Polymorphic Types :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-A954-2
%R 10.2168/LMCS-2014-1018
%U http://arxiv.org/abs/1609.08916
%D 2016
%X Many automatic theorem provers are restricted to untyped logics, and existing
translations from typed logics are bulky or unsound. Recent research proposes
monotonicity as a means to remove some clutter when translating monomorphic to
untyped first-order logic. Here we pursue this approach systematically,
analysing formally a variety of encodings that further improve on efficiency
while retaining soundness and completeness. We extend the approach to rank-1
polymorphism and present alternative schemes that lighten the translation of
polymorphic symbols based on the novel notion of "cover". The new encodings are
implemented in Isabelle/HOL as part of the Sledgehammer tool. We include
informal proofs of soundness and correctness, and have formalised the
monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new
encodings vastly superior to previous schemes.
%K Computer Science, Logic in Computer Science, cs.LO

Blanchette, J. C., Kaliszyk, C., Paulson, L. C., & Urban, J. (2016). Hammering towards QED.

*Journal of Formalized Reasoning*,*9*(1). doi:10.6092/issn.1972-5787/4593Export

BibTeX

@article{DBLP:journals/jfrea/BlanchetteKPU16,
TITLE = {Hammering towards {QED}},
AUTHOR = {Blanchette, Jasmin Christian and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef},
LANGUAGE = {eng},
ISSN = {1972-5787},
DOI = {10.6092/issn.1972-5787/4593},
YEAR = {2016},
JOURNAL = {Journal of Formalized Reasoning},
VOLUME = {9},
NUMBER = {1},
PAGES = {101--148},
}

Endnote

%0 Journal Article
%A Blanchette, Jasmin Christian
%A Kaliszyk, Cezary
%A Paulson, Lawrence C.
%A Urban, Josef
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
%T Hammering towards QED :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-3A64-6
%R 10.6092/issn.1972-5787/4593
%7 2016
%D 2016
%J Journal of Formalized Reasoning
%V 9
%N 1
%& 101
%P 101 - 148
%C Bologna
%@ false

Blanchette, J. C., & Merz, S. (Eds.). (2016).

*Interactive Theorem Proving*. Presented at the Seventh Conference on Interactive Theorem Proving, Nancy, France: Springer. doi:10.1007/978-3-319-43144-4Export

BibTeX

@proceedings{BlanchetteITP2016,
TITLE = {Interactive Theorem Proving (ITP 2016)},
EDITOR = {Blanchette, Jasmin Christian and Merz, Stephan},
LANGUAGE = {eng},
ISBN = {978-3-319-43143-7},
DOI = {10.1007/978-3-319-43144-4},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
PAGES = {XVII, 502 p.},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {9807},
ADDRESS = {Nancy, France},
}

Endnote

%0 Conference Proceedings
%E Blanchette, Jasmin Christian
%E Merz, Stephan
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Interactive Theorem Proving : 7th International Conference, ITP 2016
Nancy, France, August 22-25, 2016 ; Proceedings
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-3A6B-7
%@ 978-3-319-43143-7
%R 10.1007/978-3-319-43144-4
%I Springer
%D 2016
%B Seventh Conference on Interactive Theorem Proving
%Z date of event: 2016-08-22 - 2016-08-27
%D 2016
%C Nancy, France
%P XVII, 502 p.
%S Lecture Notes in Computer Science
%V 9807

Blanchette, J. C., & Kaliszyk, C. (Eds.). (2016).

(arXiv: 1606.05427) *Proceedings First International Workshop on Hammers for Type Theories*. Presented at the First International Workshop on Hammers for Type Theories, Coimbra, Portugal: EPTCS. doi:10.4204/EPTCS.210Export

BibTeX

@proceedings{HaTT2016,
TITLE = {Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016)},
EDITOR = {Blanchette, Jasmin Christian and Kaliszyk, Cezary},
LANGUAGE = {eng},
DOI = {10.4204/EPTCS.210},
EPRINT = {1606.05427},
EPRINTTYPE = {arXiv},
PUBLISHER = {EPTCS},
YEAR = {2016},
PAGES = {35 p.},
SERIES = {Electronic Proceedings in Theoretical Computer Science},
VOLUME = {210},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%E Blanchette, Jasmin Christian
%E Kaliszyk , Cezary
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Proceedings First International Workshop on Hammers for Type Theories :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0A70-D
%R 10.4204/EPTCS.210
%I EPTCS
%D 2016
%B First International Workshop on Hammers for Type Theories
%Z date of event: 2016-07-01 - 2016-07-01
%D 2016
%C Coimbra, Portugal
%P 35 p.
%S Electronic Proceedings in Theoretical Computer Science
%V 210
%U http://arxiv.org/abs/1606.05427

Bromberger, M. (2016).

*Analysis and Implementation of LIA solvers: CutSAT and BBSAT*. Universität des Saarlandes, Saarbrücken.Export

BibTeX

@mastersthesis{BrombergerMaster2016,
TITLE = {Analysis and Implementation of {LIA} solvers: {CutSAT} and {BBSAT}},
AUTHOR = {Bromberger, Martin},
LANGUAGE = {eng},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2016},
DATE = {2016},
}

Endnote

%0 Thesis
%A Bromberger, Martin
%Y Weidenbach, Christoph
%A referee: Sturm, Thomas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Analysis and Implementation of LIA solvers: CutSAT and BBSAT :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-410C-6
%I Universität des Saarlandes
%C Saarbrücken
%D 2016
%P 34 p.
%V master
%9 master

Bromberger, M., & Weidenbach, C. (2016a). Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. In

*Satisfiability Modulo Theories (SMT 2016)*. Coimbra, Portugal: CEUR-WS.org. Retrieved from urn:nbn:de:0074-1617-8Export

BibTeX

@inproceedings{BrombergerSMT2016,
TITLE = {Computing a Complete Basis for Equalities Implied by a System of {LRA} Constraints},
AUTHOR = {Bromberger, Martin and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {urn:nbn:de:0074-1617-8},
PUBLISHER = {CEUR-WS.org},
YEAR = {2016},
BOOKTITLE = {Satisfiability Modulo Theories (SMT 2016)},
EDITOR = {King, Tim and Piskac, Ruzica},
PAGES = {15--30},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {1617},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Computing a Complete Basis for Equalities Implied by a System of LRA Constraints :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0AA0-1
%D 2016
%B 14th International Workshop on Satisfiability Modulo Theories
%Z date of event: 2016-07-01 - 2016-07-02
%C Coimbra, Portugal
%B Satisfiability Modulo Theories
%E King, Tim; Piskac, Ruzica
%P 15 - 30
%I CEUR-WS.org
%B CEUR Workshop Proceedings
%N 1617
%@ false
%U http://ceur-ws.org/Vol-1617/paper2.pdf

Bromberger, M., & Weidenbach, C. (2016b). Fast Cube Tests for LIA Constraint Solving. In

*Automated Reasoning (IJCAR 2016)*. Coimbra, Portugal: Springer. doi:10.1007/978-3-319-40229-1_9Export

BibTeX

@inproceedings{BrombergerIJCAR2016,
TITLE = {Fast Cube Tests for {LIA} Constraint Solving},
AUTHOR = {Bromberger, Martin and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-319-40228-4},
DOI = {10.1007/978-3-319-40229-1_9},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Automated Reasoning (IJCAR 2016)},
EDITOR = {Olivetti, Nicola and Tiwari, Ashish},
PAGES = {116--132},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {9706},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Fast Cube Tests for LIA Constraint Solving :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-01C9-4
%R 10.1007/978-3-319-40229-1_9
%D 2016
%B 8th International Joint Conference on Automated Reasoning
%Z date of event: 2016-06-27 - 2016-07-02
%C Coimbra, Portugal
%B Automated Reasoning
%E Olivetti, Nicola; Tiwari, Ashish
%P 116 - 132
%I Springer
%@ 978-3-319-40228-4
%B Lecture Notes in Artificial Intelligence
%N 9706

Cruanes, S., & Blanchette, J. C. (2016). Extending Nunchaku to Dependent Type Theory. In

(arXiv: 1606.05945) *Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016)*. Coimbra, Portugal. doi:10.4204/EPTCS.210.3Abstract

Nunchaku is a new higher-order counterexample generator based on a sequence
of transformations from polymorphic higher-order logic to first-order logic.
Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone
tool, with frontends for various proof assistants. In this short paper, we
present some ideas to extend Nunchaku with partial support for dependent types
and type classes, to make frontends for Coq and other systems based on
dependent type theory more useful.

Export

BibTeX

@inproceedings{Cruanes1606.05945,
TITLE = {Extending {N}unchaku to Dependent Type Theory},
AUTHOR = {Cruanes, Simon and Blanchette, Jasmin Christian},
LANGUAGE = {eng},
ISSN = {2075-2180},
URL = {http://arxiv.org/abs/1606.05945},
DOI = {10.4204/EPTCS.210.3},
EPRINT = {1606.05945},
EPRINTTYPE = {arXiv},
YEAR = {2016},
ABSTRACT = {Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful.},
BOOKTITLE = {Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016)},
EDITOR = {Blanchette, Jasmin Christian and Kaliszyk, Cezary},
PAGES = {3--12},
SERIES = {Electronic Proceedings in Theoretical Computer Science},
VOLUME = {210},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Cruanes, Simon
%A Blanchette, Jasmin Christian
%+ Inria Nancy -- Grand Est
Automation of Logic, MPI for Informatics, Max Planck Society
%T Extending Nunchaku to Dependent Type Theory :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0A6B-E
%R 10.4204/EPTCS.210.3
%U http://arxiv.org/abs/1606.05945
%D 2016
%B First International Workshop on Hammers for Type Theories
%Z date of event: 2016-07-01 - 2016-07-01
%C Coimbra, Portugal
%X Nunchaku is a new higher-order counterexample generator based on a sequence
of transformations from polymorphic higher-order logic to first-order logic.
Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone
tool, with frontends for various proof assistants. In this short paper, we
present some ideas to extend Nunchaku with partial support for dependent types
and type classes, to make frontends for Coq and other systems based on
dependent type theory more useful.
%K Computer Science, Logic in Computer Science, cs.LO
%B Proceedings First International Workshop on Hammers for Type Theories
%E Blanchette, Jasmin Christian; Kaliszyk , Cezary
%P 3 - 12
%B Electronic Proceedings in Theoretical Computer Science
%N 210
%@ false

Fetzer, C., Weidenbach, C., & Wischnewski, P. (2016). Compliance, Functional Safety and Fault Detection by Formal Methods. In

*Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)*. Corfu, Greece: Springer. doi:10.1007/978-3-319-47169-3_48Export

BibTeX

@inproceedings{FetzerISOLA2016,
TITLE = {Compliance, Functional Safety and Fault Detection by Formal Methods},
AUTHOR = {Fetzer, Christof and Weidenbach, Christoph and Wischnewski, Patrick},
LANGUAGE = {eng},
ISBN = {978-3-319-47168-6},
DOI = {10.1007/978-3-319-47169-3_48},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)},
EDITOR = {Margaria, Tiziana and Steffen, Bernhard},
PAGES = {626--632},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {9953},
ADDRESS = {Corfu, Greece},
}

Endnote

%0 Conference Proceedings
%A Fetzer, Christof
%A Weidenbach, Christoph
%A Wischnewski, Patrick
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Compliance, Functional Safety and Fault Detection by Formal Methods :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-3A6F-0
%R 10.1007/978-3-319-47169-3_48
%D 2016
%B 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
%Z date of event: 2016-10-10 - 2016-10-14
%C Corfu, Greece
%B Leveraging Applications of Formal Methods, Verification and Validation
%E Margaria, Tiziana; Steffen, Bernhard
%P 626 - 632
%I Springer
%@ 978-3-319-47168-6
%B Lecture Notes in Computer Science
%N 9953

Košta, M., Sturm, T., & Dolzmann, A. (2016). Better Answers to Real Questions.

*Journal of Symbolic Computation*,*74*. doi:10.1016/j.jsc.2015.07.002Abstract

We consider existential problems over the reals. Extended quantifier
elimination generalizes the concept of regular quantifier elimination by
providing in addition answers, which are descriptions of possible assignments
for the quantified variables. Implementations of extended quantifier
elimination via virtual substitution have been successfully applied to various
problems in science and engineering. So far, the answers produced by these
implementations included infinitesimal and infinite numbers, which are hard to
interpret in practice. We introduce here a post-processing procedure to
convert, for fixed parameters, all answers into standard real numbers. The
relevance of our procedure is demonstrated by application of our implementation
to various examples from the literature, where it significantly improves the
quality of the results.

Export

BibTeX

@article{KostaSymbol2015,
TITLE = {Better Answers to Real Questions},
AUTHOR = {Ko{\v s}ta, Marek and Sturm, Thomas and Dolzmann, Andreas},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2015.07.002},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2016},
DATE = {2016},
ABSTRACT = {We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {74},
PAGES = {255--275},
}

Endnote

%0 Journal Article
%A Košta, Marek
%A Sturm, Thomas
%A Dolzmann, Andreas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Better Answers to Real Questions :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0026-A93B-2
%R 10.1016/j.jsc.2015.07.002
%7 2015
%D 2016
%X We consider existential problems over the reals. Extended quantifier
elimination generalizes the concept of regular quantifier elimination by
providing in addition answers, which are descriptions of possible assignments
for the quantified variables. Implementations of extended quantifier
elimination via virtual substitution have been successfully applied to various
problems in science and engineering. So far, the answers produced by these
implementations included infinitesimal and infinite numbers, which are hard to
interpret in practice. We introduce here a post-processing procedure to
convert, for fixed parameters, all answers into standard real numbers. The
relevance of our procedure is demonstrated by application of our implementation
to various examples from the literature, where it significantly improves the
quality of the results.
%K Computer Science, Symbolic Computation, cs.SC,Computer Science, Logic in Computer Science, cs.LO
%J Journal of Symbolic Computation
%V 74
%& 255
%P 255 - 275
%I Academic Press
%C London
%@ false

Košta, M. (2016).

*New Concepts for Real Quantifier Elimination by Virtual Substitution*. Universität des Saarlandes, Saarbrücken.Export

BibTeX

@phdthesis{Kostaphd16,
TITLE = {New Concepts for Real Quantifier Elimination by Virtual Substitution},
AUTHOR = {Ko{\v s}ta, Marek},
LANGUAGE = {eng},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2016},
DATE = {2016},
}

Endnote

%0 Thesis
%A Košta, Marek
%Y Sturm, Thomas
%A referee: Weber, Andreas
%A referee: Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T New Concepts for Real Quantifier Elimination by Virtual Substitution :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-30A8-9
%I Universität des Saarlandes
%C Saarbrücken
%D 2016
%P xvi, 214 p.
%V phd
%9 phd
%U http://scidok.sulb.uni-saarland.de/volltexte/2016/6716/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

Reynolds, A., & Blanchette, J. C. (2016). A Decision Procedure for (Co)datatypes in SMT Solvers. In

*Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016)*. New York, NY, USA: AAAI. Retrieved from http://www.ijcai.org/Proceedings/16/Papers/631.pdfExport

BibTeX

@inproceedings{DBLP:conf/ijcai/ReynoldsB16,
TITLE = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
AUTHOR = {Reynolds, Andrew and Blanchette, Jasmin Christian},
LANGUAGE = {eng},
ISBN = {978-1-57735-771-1},
URL = {http://www.ijcai.org/Proceedings/16/Papers/631.pdf},
PUBLISHER = {AAAI},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016)},
EDITOR = {Kambhampati, Subbarao},
PAGES = {4205--4209},
EID = {631},
ADDRESS = {New York, NY, USA},
}

Endnote

%0 Conference Proceedings
%A Reynolds, Andrew
%A Blanchette, Jasmin Christian
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Decision Procedure for (Co)datatypes in SMT Solvers :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-3A67-F
%U http://www.ijcai.org/Proceedings/16/Papers/631.pdf
%D 2016
%B 25th International Joint Conference on Artificial Intelligence
%Z date of event: 2016-07-09 - 2016-07-15
%C New York, NY, USA
%B Twenty-Fifth International Joint Conference on Artificial Intelligence
%E Kambhampati, Subbarao
%P 4205 - 4209
%Z sequence number: 631
%I AAAI
%@ 978-1-57735-771-1

Reynolds, A., Blanchette, J. C., Cruanes, S., & Tinelli, C. (2016). Model Finding for Recursive Functions in SMT. In

*Automated Reasoning (IJCAR 2016)*. Coimbra, Portugal: Springer. doi:10.1007/978-3-319-40229-1_10Export

BibTeX

@inproceedings{ReynoldsIJCAR2016,
TITLE = {Model Finding for Recursive Functions in {SMT}},
AUTHOR = {Reynolds, Andrew and Blanchette, Jasmin Christian and Cruanes, Simon and Tinelli, Cesare},
LANGUAGE = {eng},
ISBN = {978-3-319-40228-4},
DOI = {10.1007/978-3-319-40229-1_10},
PUBLISHER = {Springer},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Automated Reasoning (IJCAR 2016)},
EDITOR = {Olivetti, Nicola and Tiwari, Ashish},
PAGES = {133--151},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {9706},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Reynolds, Andrew
%A Blanchette, Jasmin Christian
%A Cruanes, Simon
%A Tinelli, Cesare
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Model Finding for Recursive Functions in SMT :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0900-2
%R 10.1007/978-3-319-40229-1_10
%D 2016
%B 8th International Joint Conference on Automated Reasoning
%Z date of event: 2016-06-27 - 2016-07-02
%C Coimbra, Portugal
%B Automated Reasoning
%E Olivetti, Nicola; Tiwari, Ashish
%P 133 - 151
%I Springer
%@ 978-3-319-40228-4
%B Lecture Notes in Artificial Intelligence
%N 9706

Sturm, T., Voigt, M., & Weidenbach, C. (2016a). Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. Retrieved from http://arxiv.org/abs/1511.08999

(arXiv: 1511.08999) Abstract

We introduce a new decidable fragment of first-order logic with equality,
which strictly generalizes two already well-known ones -- the
Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The
defining principle is the syntactic separation of universally quantified
variables from existentially quantified ones at the level of atoms. Thus, our
classification neither rests on restrictions on quantifier prefixes (as in the
BSR case) nor on restrictions on the arity of predicate symbols (as in the
monadic case). We demonstrate that the new fragment exhibits the finite model
property and derive a non-elementary upper bound on the computing time required
for deciding satisfiability in the new fragment. For the subfragment of prenex
sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the
satisfiability problem is shown to be complete for NEXPTIME. Finally, we
discuss how automated reasoning procedures can take advantage of our results.

Export

BibTeX

@online{SturmVoigtWeidenbachArXiv2016,
TITLE = {Deciding First-Order Satisfiability when Universal and Existential Variables are Separated},
AUTHOR = {Sturm, Thomas and Voigt, Marco and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1511.08999},
EPRINT = {1511.08999},
EPRINTTYPE = {arXiv},
YEAR = {2016},
ABSTRACT = {We introduce a new decidable fragment of first-order logic with equality, which strictly generalizes two already well-known ones -- the Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The defining principle is the syntactic separation of universally quantified variables from existentially quantified ones at the level of atoms. Thus, our classification neither rests on restrictions on quantifier prefixes (as in the BSR case) nor on restrictions on the arity of predicate symbols (as in the monadic case). We demonstrate that the new fragment exhibits the finite model property and derive a non-elementary upper bound on the computing time required for deciding satisfiability in the new fragment. For the subfragment of prenex sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the satisfiability problem is shown to be complete for NEXPTIME. Finally, we discuss how automated reasoning procedures can take advantage of our results.},
}

Endnote

%0 Report
%A Sturm, Thomas
%A Voigt, Marco
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Deciding First-Order Satisfiability when Universal and Existential
Variables are Separated :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4377-6
%U http://arxiv.org/abs/1511.08999
%D 2016
%X We introduce a new decidable fragment of first-order logic with equality,
which strictly generalizes two already well-known ones -- the
Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The
defining principle is the syntactic separation of universally quantified
variables from existentially quantified ones at the level of atoms. Thus, our
classification neither rests on restrictions on quantifier prefixes (as in the
BSR case) nor on restrictions on the arity of predicate symbols (as in the
monadic case). We demonstrate that the new fragment exhibits the finite model
property and derive a non-elementary upper bound on the computing time required
for deciding satisfiability in the new fragment. For the subfragment of prenex
sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the
satisfiability problem is shown to be complete for NEXPTIME. Finally, we
discuss how automated reasoning procedures can take advantage of our results.
%K Computer Science, Logic in Computer Science, cs.LO

Sturm, T., Voigt, M., & Weidenbach, C. (2016b). Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. In

*Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)*. New York, NY, USA: ACM. doi:10.1145/2933575.2934532Export

BibTeX

@inproceedings{SturmLICS2016,
TITLE = {Deciding First-Order Satisfiability when Universal and Existential Variables are Separated},
AUTHOR = {Sturm, Thomas and Voigt, Marco and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {78-1-4503-4391-6},
DOI = {10.1145/2933575.2934532},
PUBLISHER = {ACM},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)},
PAGES = {86--95},
ADDRESS = {New York, NY, USA},
}

Endnote

%0 Conference Proceedings
%A Sturm, Thomas
%A Voigt, Marco
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Deciding First-Order Satisfiability when Universal and Existential Variables are Separated :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-1B3A-F
%R 10.1145/2933575.2934532
%D 2016
%B 31st Annual ACM-IEEE Symposium on Logic in Computer Science
%Z date of event: 2016-07-05 - 2016-07-08
%C New York, NY, USA
%B Proceedings of the 31st Annual ACM-IEEE Symposium on
Logic in Computer Science
%P 86 - 95
%I ACM
%@ 78-1-4503-4391-6

Tang, C. H., & Weidenbach, C. (2016). A Dynamic Logic for Configuration. In

*Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)*. Coimbra, Portugal: CEUR-WS.org. Retrieved from http://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf; urn:nbn:de:0074-1770-7Export

BibTeX

@inproceedings{TangARQNL2016,
TITLE = {A Dynamic Logic for Configuration},
AUTHOR = {Tang, Ching Hoo and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {http://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf; urn:nbn:de:0074-1770-7},
PUBLISHER = {CEUR-WS.org},
YEAR = {2016},
BOOKTITLE = {Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)},
EDITOR = {Benzm{\"u}ller, Christoph and Otten, Jens},
PAGES = {36--50},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {1770},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Tang, Ching Hoo
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Dynamic Logic for Configuration :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4A34-D
%U http://ceur-ws.org/Vol-1770/ARQNL2016_paper3.pdf
%D 2016
%B 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics
%Z date of event: 2016-07-01 - 2016-07-01
%C Coimbra, Portugal
%B Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016)
affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)
%E Benzmüller, Christoph; Otten, Jens
%P 36 - 50
%I CEUR-WS.org
%B CEUR Workshop Proceedings
%N 1770
%@ false

Teucke, A., & Weidenbach, C. (2016). Ordered Resolution with Straight Dismatching Constraints. In

*Practical Aspects of Automated Reasoning (PAAR 2016)*. Coimbra, Portugal: CEUR-WS.org. Retrieved from urn:nbn:de:0074-1635-7Export

BibTeX

@inproceedings{Teucke_PAAR2016,
TITLE = {Ordered Resolution with Straight Dismatching Constraints},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {urn:nbn:de:0074-1635-7},
PUBLISHER = {CEUR-WS.org},
YEAR = {2016},
BOOKTITLE = {Practical Aspects of Automated Reasoning (PAAR 2016)},
EDITOR = {Fontaine, Pascal and Schulz, Stephan and Urban, Josef},
PAGES = {95--109},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {1635},
ADDRESS = {Coimbra, Portugal},
}

Endnote

%0 Conference Proceedings
%A Teucke, Andreas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Ordered Resolution with Straight Dismatching Constraints :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002B-0AB4-6
%D 2016
%B 5th Workshop on Practical Aspects of Automated Reasoning
%Z date of event: 2016-07-02 - 2016-07-02
%C Coimbra, Portugal
%B Practical Aspects of Automated Reasoning
%E Fontaine, Pascal; Schulz, Stephan; Urban, Josef
%P 95 - 109
%I CEUR-WS.org
%B CEUR Workshop Proceedings
%N 1635
%@ false
%U http://ceur-ws.org/Vol-1635/paper-09.pdf

Voigt, M. (2016a). Beyond Standard Miniscoping. In

*Deduktionstreffen 2016*. Klagenfurt, Austria.Export

BibTeX

@inproceedings{VoigtDeduktionstreffen2016,
TITLE = {Beyond Standard Miniscoping},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
YEAR = {2016},
BOOKTITLE = {Deduktionstreffen 2016},
ADDRESS = {Klagenfurt, Austria},
}

Endnote

%0 Conference Proceedings
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Beyond Standard Miniscoping :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4397-D
%D 2016
%B Deduktionstreffen 2016
%Z date of event: 2016-09-26 - 2016-09-26
%C Klagenfurt, Austria
%B Deduktionstreffen 2016
%U https://fg-dedsys.gi.de/fileadmin/user_upload/dt2016/voigt.pdf

Voigt, M. (2016b). The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond. In

*Seventeenth International Workshop on Logic and Computational Complexity (LCC 2016)*. Marseille, France.Export

BibTeX

@inproceedings{VoigtLCC2016,
TITLE = {The Complexity of Satisfiability in the Separated Fragment -- A Journey Through {ELEMENTARY} and Beyond},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
YEAR = {2016},
DATE = {2016},
BOOKTITLE = {Seventeenth International Workshop on Logic and Computational Complexity (LCC 2016)},
PAGES = {43--47},
ADDRESS = {Marseille, France},
}

Endnote

%0 Conference Proceedings
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4392-8
%D 2016
%B Seventeenth International Workshop on Logic and Computational Complexity
%Z date of event: 2016-09-02 - 2016-09-03
%C Marseille, France
%B Seventeenth International Workshop on Logic and Computational Complexity
%P 43 - 47
%U http://csl16.lif.univ-mrs.fr/static/media/talk82/slides_website_version.pdf

Wand, D. (2016).

*More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification*. Universität des Saarlandes, Saarbrücken.Export

BibTeX

@mastersthesis{WandMaster2016,
TITLE = {More {SPASS} with {I}sabelle -- {S}uperposition with {H}ard {S}orts and {C}onfigurable {S}implification},
AUTHOR = {Wand, Daniel},
LANGUAGE = {eng},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2016},
DATE = {2016},
}

Endnote

%0 Thesis
%A Wand, Daniel
%Y Weidenbach, Christoph
%A referee: Waldmann, Uwe
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-AC8E-1
%I Universität des Saarlandes
%C Saarbrücken
%D 2016
%P 22 p.
%V master
%9 master