Algorithms for the Undecided SS2015

News | Content | Grading | Time schedule | Material

Explanation

Each student will be assigned a paper from the following list and prepare a presentation about it under the supervision of a member of the chair. Note that some notions presented in these papers have a reasonably nice summary on wikipedia.

List of papers

[1]

Orly Meir and Ofer Strichman. Yet another decision procedure for equality logic. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, pages 307-320, 2005. [ PDF ]

[2]

Felix Klaedtke. Bounds on the automata size for presburger arithmetic. ACM Trans. Comput. Log., 9(2), 2008. [ PDF ]

[3]

Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identifications. Combinatorica, 12(4):389-410, 1992. [ PDF ]

[4]

Jonathan A. Kelner and Daniel A. Spielman. A randomized polynomial-time simplex algorithm for linear programming. In Proceedings of the 38th Annual ACM Symposium on Theory of Computing, Seattle, WA, USA, May 21-23, 2006, pages 51-60, 2006. [ PDF ]

[5]

Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, pages 114-128, 2012. [ PDF ]

[6]

Kenneth L. McMillan. An interpolating theorem prover. Theor. Comput. Sci., 345(1):101-121, 2005. [ PDF ]

[7]

Marcin Jurdzinski. Small progress measures for solving parity games. In STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, pages 290-301, 2000. [ PDF ]

[8]

Zohar Manna and Calogero G Zarba. Combining decision procedures. In Formal Methods at the Crossroads. From Panacea to Foundational Support, pages 381-422. Springer, 2003. [ PDF ]

[9]

Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving sat and sat modulo theories: From an abstract davis-putnam-logemann-loveland procedure to dpll(t). J. ACM, 53(6):937-977, November 2006. [ PDF ]

[10]

Dejan Jovanovic and Leonardo Mendonça de Moura. Solving non-linear arithmetic. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, pages 339-354, 2012. [ PDF ]

[11]

Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A decidable fragment of separation logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, pages 97-109, 2004. [ PDF ]

[12]

Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. A type-directed abstraction refinement approach to higher-order model checking. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 61-72, 2014. [ PDF ]