Martin Brain

59 papers A 1B 14C 4Journal 17Unranked 21
YearRankTypeTitle / Venue / Authors
2026 J jnl
Canonical Forms and Widening for Two Variables Per Inequality Systems.
Math. Comput. Sci.
Martin Brain, Jacob M. Howe
2024 — conf
A Pyramid Of (Formal) Software Verification.
FM (2)
Martin Brain, Elizabeth Polgreen
2024 — conf
Misconceptions about Loops in C.
SOAP@PLDI
Martin Brain, Mahdi Malkawi
2023 J jnl
Verifying Classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation.
IACR Cryptol. ePrint Arch.
Martin Brain, Carlos Cid, Rachel Player, Wrenna Robson
2023 — conf
Widening for Systems of Two Variables Per Inequality.
SC-Square@ISSAC
Martin Brain, Jacob M. Howe
2022 — conf
Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation.
CBCrypto
Martin Brain, Carlos Cid, Rachel Player, Wrenna Robson
2022 — conf
cvc5: A Versatile and Industrial-Strength SMT Solver.
TACAS (1)
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
2021 — conf
Further Steps Down The Wrong Path: Improving the Bit-Blasting of Multiplication.
SMT
Martin Brain
2019 B conf
Application of Abstract Interpretation to the Automotive Electronic Control System.
VMCAI
Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura
2019 — conf
Building Better Bit-Blasting for Floating-Point Problems.
TACAS (1)
Martin Brain, Florian Schanda, Youcheng Sun
2019 — conf
Invertibility Conditions for Floating-Point Formulas.
CAV (2)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Verifying Reachability Properties in Markov Chains via Incremental Induction.
CoRR
Elizabeth Polgreen, Martin Brain, Martin Fränzle, Alessandro Abate
2018 J jnl
CVC4 at the SMT Competition 2018.
CoRR
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018 — ed.
Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference, SC-Square@FLOC 2018, Oxford, UK, July 11, 2018.
SC-Square@FLOC
Anna Maria Bigatti, Martin Brain
2017 — conf
Benchmarking Solvers, SAT-style.
SC²@ISSAC
Martin Brain, James H. Davenport, Alberto Griggio
2017 B conf
Functional Requirements-Based Automated Testing for Avionics.
ICECCS
Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzman Jimenez, Simon Daniel, Chris Bryan, Ian Broster
2017 J jnl
Functional Requirements-Based Automated Testing for Avionics.
CoRR
Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzman Jimenez, Simon Daniel, Chris Bryan, Ian Broster
2017 J jnl
Incremental bounded model checking for embedded software.
Formal Aspects Comput.
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2017 — ed.
Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22 - 23, 2017.
SMT
Martin Brain, Liana Hadarean
2017 — conf
SC-square: when Satisfiability Checking and Symbolic Computation join forces.
ARCADE@CADE
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler
2016 — conf
Algebraic Techniques in Software Verification : Challenges and Opportunities.
SC²@SYNASC
Martin Brain, Daniel Kroening, Ryan McCleeary
2016 B conf
Automatic Generation of Propagation Complete SAT Encodings.
VMCAI
Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins
2016 C conf
SC
CICM
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability Checking and Symbolic Computation.
CoRR
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability Checking meets Symbolic Computation (Project Paper).
CoRR
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability checking and symbolic computation.
ACM Commun. Comput. Algebra
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 — conf
Towards Automated Bounded Model Checking of API Implementations.
CSTVA@ISSTA
Daniel Neville, Andrew J. Malton, Martin Brain, Daniel Kroening
2015 J jnl
A lazy approach to adaptive exact real arithmetic using floating-point operations.
ACM Commun. Comput. Algebra
Ryan McCleeary, Martin Brain, Aaron Stump
2015 C conf
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.
ARITH
Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
2015 B conf
Safety Verification and Refutation by k-Invariants and k-Induction.
SAS
Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel
2015 J jnl
Safety Verification and Refutation by k-invariants and k-induction (extended version).
CoRR
Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel
2015 C conf
Successful Use of Incremental BMC in the Automotive Industry.
FMICS
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2014 J jnl
Deciding floating-point logic with abstract conflict driven clause learning.
Formal Methods Syst. Des.
Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
2014 J jnl
Incremental Bounded Model Checking for Embedded Software (extended version).
CoRR
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller
2014 A conf
Model and Proof Generation for Heap-Manipulating Programs.
ESOP
Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel
2013 B conf
An Abstract Interpretation of DPLL(T).
VMCAI
Martin Brain, Vijay Victor D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening
2013 B conf
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL.
SAS
Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening
2012 — conf
A Lightweight Technique for Distributed and Incremental Program Verification.
VSTTE
Martin Brain, Florian Schanda
2012 — conf
Computational Music Theory.
MUME@AIIDE
Georg Boenn, Martin Brain, Marina De Vos, John ffitch
2012 B conf
Deciding floating-point logic with systematic abstraction.
FMCAD
Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening
2012 C conf
Simplifying the Verification of Quantified Array Assertions via Code Transformation.
LOPSTR
Mohamed Nassim Seghir, Martin Brain
2012 — conf
Using Answer Set Programming in the Development of Verified Software.
ICLP (Technical Communications)
Florian Schanda, Martin Brain
2011 — conf
Anton - A Rule-Based Composition System.
ICMC
Georg Boenn, Martin Brain, Marina De Vos, John ffitch
2011 J jnl
Automatic music composition using answer set programming.
Theory Pract. Log. Program.
Georg Boenn, Martin Brain, Marina De Vos, John P. Fitch
2010 J jnl
A new-generation automated warehousing capability.
Int. J. Comput. Integr. Manuf.
Qian Wang, Richard McIntosh, Martin Brain
2010 J jnl
Automatic Music Composition using Answer Set Programming
CoRR
Georg Boenn, Martin Brain, Marina De Vos, John ffitch
2009 B conf
ANTON: Composing Logic and Logic Composing.
LPNMR
Georg Boenn, Martin Brain, Marina De Vos, John ffitch
2009 B conf
Generating Optimal Code Using Answer Set Programming.
LPNMR
Tom Crick, Martin Brain, Marina De Vos, John P. Fitch
2009 J jnl
The Significance of Memory Costs in Answer Set Solver Implementation.
J. Log. Comput.
Martin Brain, Marina De Vos
2008 B conf
ASPVIZ: Declarative Visualisation and Animation Using Answer Set Programming.
ICLP
Owen Cliffe, Marina De Vos, Martin Brain, Julian A. Padget
2008 — conf
Answer Set Programming ? a Domain in Need of Explanation: A Position Paper.
ExaCt
Martin Brain, Marina De Vos
2008 B conf
Automatic Composition of Melodic and Harmonic Music by Answer Set Programming.
ICLP
Georg Boenn, Martin Brain, Marina De Vos, John ffitch
2007 B conf
Debugging ASP Programs by Means of ASP.
LPNMR
Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, Stefan Woltran
2006 B conf
Declarative Problem Solving Using Answer Set Semantics.
ICLP
Martin Brain
2006 B conf
TOAST: Applying Answer Set Programming to Superoptimisation.
ICLP
Martin Brain, Tom Crick, Marina De Vos, John P. Fitch
2005 — conf
An Interactive Approach to Answer Set Programming.
Answer Set Programming
Martin Brain, Richard Watson, Marina De Vos
2005 — conf
Debugging Logic Programs under the Answer Set Semantics.
Answer Set Programming
Martin Brain, Marina De Vos
2005 — conf
LAIMA: A Multi-agent Platform Using Ordered Choice Logic Programming.
DALT
Marina De Vos, Tom Crick, Julian A. Padget, Martin Brain, Owen Cliffe, Jonathan Needham
2003 — conf
Implementing OCLP as a front-end for Answer Set Solvers: From Theory to Practice.
Answer Set Programming
Martin Brain, Marina De Vos