Martin Brain

According to our database, Martin Brain authored at least 52 papers between 2003 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Misconceptions about Loops in C.

Martin Brain, Mahdi Malkawi

Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, 2024

A Pyramid Of (Formal) Software Verification.

Martin Brain, Elizabeth Polgreen

Proceedings of the Formal Methods - 26th International Symposium, 2024

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

Widening for Systems of Two Variables Per Inequality.

Martin Brain, Jacob M. Howe

Proceedings of the 8th SC-Square Workshop co-located with the 48th International Symposium on Symbolic and Algebraic Computation, 2023

2022

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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

2021

Further Steps Down The Wrong Path: Improving the Bit-Blasting of Multiplication.

Martin Brain

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

2019

Verifying Reachability Properties in Markov Chains via Incremental Induction.

Elizabeth Polgreen, Martin Brain, Martin Fränzle, Alessandro Abate

CoRR, 2019

Application of Abstract Interpretation to the Automotive Electronic Control System.

Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, Yoshiumi Kawamura

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

Building Better Bit-Blasting for Floating-Point Problems.

Martin Brain, Florian Schanda, Youcheng Sun

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Invertibility Conditions for Floating-Point Formulas.

Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

CVC4 at the SMT Competition 2018.

Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli

CoRR, 2018

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

Benchmarking Solvers, SAT-style.

Martin Brain, James H. Davenport, Alberto Griggio

Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 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

Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017

SC-square: when Satisfiability Checking and Symbolic Computation join forces.

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

Proceedings of the ARCADE 2017, 2017

2016

Satisfiability Checking meets Symbolic Computation (Project Paper).

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

CoRR, 2016

Satisfiability checking and symbolic computation.

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

ACM Commun. Comput. Algebra, 2016

Automatic Generation of Propagation Complete SAT Encodings.

Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Algebraic Techniques in Software Verification : Challenges and Opportunities.

Martin Brain, Daniel Kroening, Ryan McCleeary

Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation co-located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), 2016

SC²: Satisfiability Checking Meets Symbolic Computation - (Project Paper).

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

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Towards Automated Bounded Model Checking of API Implementations.

Daniel Neville, Andrew J. Malton, Martin Brain, Daniel Kroening

Proceedings of the 7th Workshop on Constraint Solvers in Testing, 2016

2015

Safety Verification and Refutation by k-invariants and k-induction (extended version).

Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel

CoRR, 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.

Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel

Proceedings of the Static Analysis - 22nd International Symposium, 2015

Successful Use of Incremental BMC in the Automotive Industry.

Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller

Proceedings of the Formal Methods for Industrial Critical Systems, 2015

An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic.

Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl

Proceedings of the 22nd IEEE Symposium on Computer Arithmetic, 2015

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

Incremental Bounded Model Checking for Embedded Software (extended version).

Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller

CoRR, 2014

Model and Proof Generation for Heap-Manipulating Programs.

Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel

Proceedings of the Programming Languages and Systems, 2014

2013

An Abstract Interpretation of DPLL(T).

Martin Brain, Vijay Victor D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening

Proceedings of the Verification, 2013

Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL.

Martin Brain, Vijay Victor D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening

Proceedings of the Static Analysis - 20th International Symposium, 2013

2012

A Lightweight Technique for Distributed and Incremental Program Verification.

Martin Brain, Florian Schanda

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Simplifying the Verification of Quantified Array Assertions via Code Transformation.

Mohamed Nassim Seghir, Martin Brain

Proceedings of the Logic-Based Program Synthesis and Transformation, 2012

Using Answer Set Programming in the Development of Verified Software.

Florian Schanda, Martin Brain

Proceedings of the Technical Communications of the 28th International Conference on Logic Programming, 2012

Deciding floating-point logic with systematic abstraction.

Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening

Proceedings of the Formal Methods in Computer-Aided Design, 2012

Computational Music Theory.

Georg Boenn, Martin Brain, Marina De Vos, John ffitch

Proceedings of the Musical Metacreation, 2012

2011

Automatic music composition using answer set programming.

Georg Boenn, Martin Brain, Marina De Vos, John P. Fitch

Theory Pract. Log. Program., 2011

Anton - A Rule-Based Composition System.

Georg Boenn, Martin Brain, Marina De Vos, John ffitch

Proceedings of the 2011 International Computer Music Conference, 2011

2010

A new-generation automated warehousing capability.

Qian Wang, Richard McIntosh, Martin Brain

Int. J. Comput. Integr. Manuf., 2010

2009

The Significance of Memory Costs in Answer Set Solver Implementation.

Martin Brain, Marina De Vos

J. Log. Comput., 2009

Generating Optimal Code Using Answer Set Programming.

Tom Crick, Martin Brain, Marina De Vos, John P. Fitch

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2009

ANTON: Composing Logic and Logic Composing.

Georg Boenn, Martin Brain, Marina De Vos, John ffitch

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2009

2008

ASPVIZ: Declarative Visualisation and Animation Using Answer Set Programming.

Owen Cliffe, Marina De Vos, Martin Brain, Julian A. Padget

Proceedings of the Logic Programming, 24th International Conference, 2008

Automatic Composition of Melodic and Harmonic Music by Answer Set Programming.

Georg Boenn, Martin Brain, Marina De Vos, John ffitch

Proceedings of the Logic Programming, 24th International Conference, 2008

Answer Set Programming ? a Domain in Need of Explanation: A Position Paper.

Martin Brain, Marina De Vos

Proceedings of the Explanation-aware Computing, 2008

2007

Debugging ASP Programs by Means of ASP.

Martin Brain, Martin Gebser, Jörg Pührer, Torsten Schaub, Hans Tompits, Stefan Woltran

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2007

2006

TOAST: Applying Answer Set Programming to Superoptimisation.

Martin Brain, Tom Crick, Marina De Vos, John P. Fitch

Proceedings of the Logic Programming, 22nd International Conference, 2006

Declarative Problem Solving Using Answer Set Semantics.

Martin Brain

Proceedings of the Logic Programming, 22nd International Conference, 2006

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

Proceedings of the Declarative Agent Languages and Technologies III, 2005

An Interactive Approach to Answer Set Programming.

Martin Brain, Richard Watson, Marina De Vos

Proceedings of the Answer Set Programming, 2005

Debugging Logic Programs under the Answer Set Semantics.

Martin Brain, Marina De Vos

Proceedings of the Answer Set Programming, 2005

2003

Implementing OCLP as a front-end for Answer Set Solvers: From Theory to Practice.

Martin Brain, Marina De Vos

Proceedings of the Answer Set Programming, 2003