@inproceedings{d2014abstract, title = "Abstract satisfaction", author = "D'Silva, Vijay and Haller, Leopold and Kroening, Daniel", year = "2014", booktitle = "Proceedings of the 41st annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages", organization = "ACM", pages = "139--150", } @article{brain2013deciding, title = "Deciding floating-point logic with abstract conflict driven clause learning", author = "Brain, Martin and D’Silva, Vijay and Griggio, Alberto and Haller, Leopold and Kroening, Daniel", year = "2013", journal = "Formal Methods in System Design", pages = "1--33", publisher = "Springer US", } @incollection{brain2013interpolation, title = "Interpolation-based verification of floating-point programs with abstract CDCL", author = "Brain, Martin and D’Silva, Vijay and Griggio, Alberto and Haller, Leopold and Kroening, Daniel", year = "2013", booktitle = "Static Analysis", pages = "412--432", publisher = "Springer Berlin Heidelberg", } @inproceedings{our-work.POPL:2013, title = "Abstract Conflict Driven Learning", author = "V. D'Silva and L. Haller and D. Kroening", year = "2013", booktitle = "Proc.~of the Symposium on Principles of Programming Languages", publisher = "ACM", } @inproceedings{our-work.VMCAI:2013, title = "An Abstract Interpretation of {DPLL(T)}", author = "M. Brain and V. D'Silva and L. Haller and A. Griggio and D. Kroening", year = "2013", booktitle = "Proc.~of the conference on Verification, Model Checking and Abstract Interpretation", } @inproceedings{our-work.SAS:2012, title = "Satisfiability Solvers are Static Analysers", author = "V. D'Silva and L. Haller and D. Kroening", year = "2012", booktitle = "Proc.~of Static Analysis Symposium", pages = "317-333", publisher = "Springer", } @inproceedings{our-work.FMCAD:2012, title = "Deciding Floating-Point Logic with Systematic Abstraction", author = "L. Haller and A. Griggio, and M. Brain, and D. Kroening", year = "2012", booktitle = "FMCAD", url = "http://www.cs.ox.ac.uk/people/leopold.haller/papers/fmcad2012.pdf", } @inproceedings{dhkt.tacas.2012, title = "Numeric Bounds Analysis with Conflict-Driven Learning", author = "Vijay D'Silva and Leopold Haller and Daniel Kroening and Michael Tautschnig", year = "2012", booktitle = "TACAS", url = "https://www.cs.ox.ac.uk/people/leopold.haller/papers/tacas2012.pdf", } @inproceedings{DBLP:conf/vmcai/DonaldsonHK11, title = "Strengthening Induction-Based Race Checking with Lightweight Static Analysis", author = "Alastair F. Donaldson and Leopold Haller and Daniel Kroening", year = "2011", booktitle = "VMCAI", pages = "169-183", } @inproceedings{DonaldsonHKR_SAS2011, title = "Software Verification Using k-Induction", author = "Alastair F. Donaldson and Leopold Haller and Daniel Kroening and Philipp Ruemmer", year = "2011", booktitle = "SAS", publisher = "Springer", series = "Lecture Notes in Computer Science", } @article{DBLP:journals/ki/EglyH10, title = "A SAT Solver for Circuits Based on the Tableau Method", author = "Uwe Egly and Leopold Haller", year = "2010", journal = "KI", number = "1", pages = "15-23", volume = "24", } @inproceedings{DBLP:conf/fmcad/HallerS10, title = "Relieving capacity limits on FPGA-based SAT-solvers", author = "Leopold Haller and Satnam Singh", year = "2010", booktitle = "FMCAD", pages = "217-220", } @inproceedings{DBLP:conf/sat/ChebiryakWKH09, title = "Finding Lean Induced Cycles in Binary Hypercubes", author = "Yury Chebiryak and Thomas Wahl and Daniel Kroening and Leopold Haller", year = "2009", booktitle = "SAT", pages = "18-31", }