Implementing OCLP as a front-end for Answer Set Solvers: From Theory to Practice. - Martin Brain; Marina De Vos (Answer Set Programming, 2003)

Debugging Logic Programs under the Answer Set Semantics. - Martin Brain; Marina De Vos (Answer Set Programming, 2005)

An Interactive Approach to Answer Set Programming. - Martin Brain; Richard Watson 003; Marina De Vos (Answer Set Programming, 2005)

LAIMA: A Multi-agent Platform Using Ordered Choice Logic Programming. - Marina De Vos; Tom Crick; Julian A. Padget; Martin Brain; Owen Cliffe; Jonathan Needham (DALT, 2005)

Declarative Problem Solving Using Answer Set Semantics. - Martin Brain (ICLP, 2006)

TOAST: Applying Answer Set Programming to Superoptimisation. - Martin Brain; Tom Crick; Marina De Vos; John P. Fitch (ICLP, 2006)

Debugging ASP Programs by Means of ASP. - Martin Brain; Martin Gebser; Jörg Pührer; Torsten Schaub; Hans Tompits; Stefan Woltran (LPNMR, 2007)

Answer Set Programming ? a Domain in Need of Explanation: A Position Paper. - Martin Brain; Marina De Vos (ExaCt, 2008)

Automatic Composition of Melodic and Harmonic Music by Answer Set Programming. - Georg Boenn; Martin Brain; Marina De Vos; John ffitch (ICLP, 2008)

ASPVIZ: Declarative Visualisation and Animation Using Answer Set Programming. - Owen Cliffe; Marina De Vos; Martin Brain; Julian A. Padget (ICLP, 2008)

ANTON: Composing Logic and Logic Composing. - Georg Boenn; Martin Brain; Marina De Vos; John ffitch (LPNMR, 2009)

Generating Optimal Code Using Answer Set Programming. - Tom Crick; Martin Brain; Marina De Vos; John P. Fitch (LPNMR, 2009)

The Significance of Memory Costs in Answer Set Solver Implementation. - Martin Brain; Marina De Vos (J. Log. Comput., 2009)

A new-generation automated warehousing capability. - Qian Wang; Richard McIntosh; Martin Brain (Int. J. Comput. Integr. Manuf., 2010)

Anton - A Rule-Based Composition System. - Georg Boenn; Martin Brain; Marina De Vos; John ffitch (ICMC, 2011)

Automatic music composition using answer set programming. - Georg Boenn; Martin Brain; Marina De Vos; John P. Fitch (Theory Pract. Log. Program., 2011)

Computational Music Theory. - Georg Boenn; Martin Brain; Marina De Vos; John ffitch (MUME@AIIDE, 2012)

Deciding floating-point logic with systematic abstraction. - Leopold Haller; Alberto Griggio; Martin Brain; Daniel Kroening (FMCAD, 2012)

Using Answer Set Programming in the Development of Verified Software. - Florian Schanda; Martin Brain (ICLP (Technical Communications), 2012)

Simplifying the Verification of Quantified Array Assertions via Code Transformation. - Mohamed Nassim Seghir; Martin Brain (LOPSTR, 2012)

A Lightweight Technique for Distributed and Incremental Program Verification. - Martin Brain; Florian Schanda (VSTTE, 2012)

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (SAS, 2013)

An Abstract Interpretation of DPLL(T). - Martin Brain; Vijay Victor D'Silva; Leopold Haller; Alberto Griggio; Daniel Kroening (VMCAI, 2013)

Model and Proof Generation for Heap-Manipulating Programs. - Martin Brain; Cristina David; Daniel Kroening; Peter Schrammel (ESOP, 2014)

Incremental Bounded Model Checking for Embedded Software (extended version). - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (CoRR, 2014)

Deciding floating-point logic with abstract conflict driven clause learning. - Martin Brain; Vijay Victor D'Silva; Alberto Griggio; Leopold Haller; Daniel Kroening (Formal Methods Syst. Des., 2014)

An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. - Martin Brain; Cesare Tinelli; Philipp Rümmer; Thomas Wahl (ARITH, 2015)

Successful Use of Incremental BMC in the Automotive Industry. - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (FMICS, 2015)

Safety Verification and Refutation by k-Invariants and k-Induction. - Martin Brain; Saurabh Joshi 001; Daniel Kroening; Peter Schrammel (SAS, 2015)

A lazy approach to adaptive exact real arithmetic using floating-point operations. - Ryan McCleeary; Martin Brain; Aaron Stump (ACM Commun. Comput. Algebra, 2015)

Safety Verification and Refutation by k-invariants and k-induction (extended version). - Martin Brain; Saurabh Joshi 001; Daniel Kroening; Peter Schrammel (CoRR, 2015)

Towards Automated Bounded Model Checking of API Implementations. - Daniel Neville; Andrew J. Malton; Martin Brain; Daniel Kroening (CSTVA@ISSTA, 2016)

SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CICM, 2016)

Algebraic Techniques in Software Verification : Challenges and Opportunities. - Martin Brain; Daniel Kroening; Ryan McCleeary (SC²@SYNASC, 2016)

Automatic Generation of Propagation Complete SAT Encodings. - Martin Brain; Liana Hadarean; Daniel Kroening; Ruben Martins (VMCAI, 2016)

Satisfiability checking and symbolic computation. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (ACM Commun. Comput. Algebra, 2016)

Satisfiability Checking meets Symbolic Computation (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CoRR, 2016)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Functional Requirements-Based Automated Testing for Avionics. - Youcheng Sun; Martin Brain; Daniel Kroening; Andrew Hawthorn; Thomas Wilson; Florian Schanda; Francisco Javier Guzman Jimenez; Simon Daniel; Chris Bryan; Ian Broster (ICECCS, 2017)

Benchmarking Solvers, SAT-style. - Martin Brain; James H. Davenport; Alberto Griggio (SC²@ISSAC, 2017)

Incremental bounded model checking for embedded software. - Peter Schrammel; Daniel Kroening; Martin Brain; Ruben Martins; Tino Teige; Tom Bienmüller (Formal Aspects Comput., 2017)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

Invertibility Conditions for Floating-Point Formulas. - Martin Brain; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

Building Better Bit-Blasting for Floating-Point Problems. - Martin Brain; Florian Schanda; Youcheng Sun (TACAS (1), 2019)

Application of Abstract Interpretation to the Automotive Electronic Control System. - Tomoya Yamaguchi 001; Martin Brain; Chirs Ryder; Yosikazu Imai; Yoshiumi Kawamura (VMCAI, 2019)

Verifying Reachability Properties in Markov Chains via Incremental Induction. - Elizabeth Polgreen; Martin Brain; Martin Fränzle; Alessandro Abate (CoRR, 2019)

Further Steps Down The Wrong Path: Improving the Bit-Blasting of Multiplication. - Martin Brain (SMT, 2021)

cvc5: A Versatile and Industrial-Strength SMT Solver. - 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; et al. (TACAS (1), 2022)

Widening for Systems of Two Variables Per Inequality. - Martin Brain; Jacob M. Howe (SC-Square@ISSAC, 2023)

Verifying Classic McEliece: examining the role of formal methods in post-quantum cryptography standardisation. - Martin Brain; Carlos Cid; Rachel Player; Wrenna Robson (IACR Cryptol. ePrint Arch., 2023)

A Pyramid Of (Formal) Software Verification. - Martin Brain; Elizabeth Polgreen (FM (2), 2024)

Misconceptions about Loops in C. - Martin Brain; Mahdi Malkawi (SOAP@PLDI, 2024)