Last Year

Á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.3055285
Export
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}, MARGINALMARK = {$\bullet$}, 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). SC2: Satisfiability Checking Meets Symbolic Computation. In Intelligent Computer Mathematics (CICM 2016). Bialystok, Poland: Springer. doi:10.1007/978-3-319-42547-4_3
Export
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}, MARGINALMARK = {$\bullet$}, 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. (2016c). 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}, MARGINALMARK = {$\bullet$}, 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
Ábrahám, E., Abbott, J., Becker, B., Bigatti, A. M., Brain, M., Buchberger, B., … Sturm, T. (2016d). 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}, MARGINALMARK = {$\bullet$}, 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
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}, MARGINALMARK = {$\bullet$}, 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-67309
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
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}, MARGINALMARK = {$\bullet$}, 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_5
Export
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}, MARGINALMARK = {$\bullet$}, 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., 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}, MARGINALMARK = {$\bullet$}, 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/4593
Export
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}, MARGINALMARK = {$\bullet$}, 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., 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-8
Export
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}, MARGINALMARK = {$\bullet$}, 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., 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-3
Export
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}, MARGINALMARK = {$\bullet$}, 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., & Kaliszyk, C. (Eds.). (2016). 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.210
(arXiv: 1606.05427)
Export
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}, MARGINALMARK = {$\bullet$}, 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
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-4
Export
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}, MARGINALMARK = {$\bullet$}, 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., 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_4
Export
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}, MARGINALMARK = {$\bullet$}, 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
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-8
Export
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}, MARGINALMARK = {$\bullet$}, 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_9
Export
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}, MARGINALMARK = {$\bullet$}, 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
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}, MARGINALMARK = {$\bullet$}, 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
Cruanes, S., & Blanchette, J. C. (2016). Extending Nunchaku to Dependent Type Theory. In Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016). Coimbra, Portugal. doi:10.4204/EPTCS.210.3
(arXiv: 1606.05945)
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.
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}, MARGINALMARK = {$\bullet$}, 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_48
Export
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}, MARGINALMARK = {$\bullet$}, 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.002
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.
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}, MARGINALMARK = {$\bullet$}, 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}, MARGINALMARK = {$\bullet$}, 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/doku/lic_ohne_pod.php?la=dehttp://scidok.sulb.uni-saarland.de/volltexte/2016/6716/
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_10
Export
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}, MARGINALMARK = {$\bullet$}, 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
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.pdf
Export
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}, MARGINALMARK = {$\bullet$}, 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
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}, MARGINALMARK = {$\bullet$}, 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.2934532
Export
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}, MARGINALMARK = {$\bullet$}, 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-7
Export
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}, MARGINALMARK = {$\bullet$}, 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-7
Export
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}, MARGINALMARK = {$\bullet$}, 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). 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}, MARGINALMARK = {$\bullet$}, 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
Voigt, M. (2016b). Beyond Standard Miniscoping. In Deduktionstreffen 2016. Klagenfurt, Austria.
Export
BibTeX
@inproceedings{VoigtDeduktionstreffen2016, TITLE = {Beyond Standard Miniscoping}, AUTHOR = {Voigt, Marco}, LANGUAGE = {eng}, YEAR = {2016}, MARGINALMARK = {$\bullet$}, 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
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}, MARGINALMARK = {$\bullet$}, 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