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
Á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
Á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)
Á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)
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.
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
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
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)
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
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
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
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)
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
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
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
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
Bromberger, M. (2016). Analysis and Implementation of LIA solvers: CutSAT and BBSAT. Universität des Saarlandes, Saarbrücken.
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)
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
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
Košta, M. (2016). New Concepts for Real Quantifier Elimination by Virtual Substitution. Universität des Saarlandes, Saarbrücken.
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
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
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)
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
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
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
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.
Voigt, M. (2016b). Beyond Standard Miniscoping. In Deduktionstreffen 2016. Klagenfurt, Austria.
Wand, D. (2016). More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. Universität des Saarlandes, Saarbrücken.