Martin Brain

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 28

Top Topics

Clause Learning

Bounded Model Checking

Sparse Matrices

Floating Point Arithmetic

Top Venues

ACM Commun. Comput. Algebra

Publications

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