Search

Martin Nyx Brain

Lecturer in Computer Science

School of Science and TechnologyDepartment of Computer Science

Contact details

Address

Martin Nyx Brain A309C, College Building
City, University of London
Northampton Square
London EC1V 0HB
United Kingdom

About

Overview

Martin's work is broadly within the areas of automated reasoning and automated verification for safety and security. On the automated reasoning side he mostly works on SAT / SMT solvers, including being the co-author of the SMT-LIB theory of floating-point and developing the CVC4 floating-point theory solver. In automated verification he mainly focuses on low-level and embedded software in C, C++ and Ada using a combination of abstract interpretation, symbolic execution and deductive verification and tools including SPARK and CBMC / CPROVER.

Publications

Publications by category

Chapter

  • Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M. … Zohar, Y. (2022). cvc5: A Versatile and Industrial-Strength SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems (pp. 415–442). Springer International Publishing. ISBN 978-3-030-99523-2.

Conference papers and proceedings (22)

  • Brain, M., Schanda, F. and Sun, Y. (2019). Building Better Bit-Blasting for Floating-Point Problems.
  • Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C. and Tinelli, C. (2019). Invertibility Conditions for Floating-Point Formulas.
  • Sun, Y., Broster, I., Brain, M., Kroening, D., Hawthorn, A., Wilson, T. … Bryan, C. (2017). Functional Requirements-Based Automated Testing for Avionics. 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS) 5-8 November.
  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Cimatti, A. … Seiler, W.M. (2017). SC-square: when Satisfiability Checking and Symbolic Computation join forces.
  • Sun, Y., Brain, M., Kroening, D., Hawthorn, A., Wilson, T., Schanda, F. … Broster, I. (2017). Functional Requirements-Based Automated Testing for Avionics.
  • Brain, M., Kroening, D. and McCleeary, R. (2016). Algebraic techniques in software verification : Challenges and opportunities.
  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B. … Sturm, T. (2016). $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation.
  • Neville, D., Malton, A., Brain, M. and Kroening, D. (2016). Towards automated bounded model checking of API implementations.
  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B. … Sturm, T. (2016). SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper).
  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B. … Sturm, T. (2016). SC2: Satisfiability checking meets symbolic computation (Project Paper).
  • Brain, M., Hadarean, L., Kroening, D. and Martins, R. (2016). Automatic Generation of Propagation Complete SAT Encodings.
  • Brain, M., Tinelli, C., Ruemmer, P. and Wahl, T. (2015). An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. 2015 IEEE 22nd Symposium on Computer Arithmetic (ARITH) 22-24 June.
  • Brain, M., Joshi, S., Kroening, D. and Schrammel, P. (2015). Safety Verification and Refutation by k-invariants and k-induction. Static Analysis.
  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T. and Bienmüller, T. (2015). Successful Use of Incremental BMC in the Automotive Industry.
  • Brain, M., Joshi, S., Kroening, D. and Schrammel, P. (2015). Safety Verification and Refutation by k-Invariants and k-Induction.
  • Brain, M., David, C., Kroening, D. and Schrammel, P. (2014). Model and Proof Generation for Heap-Manipulating Programs.
  • Brain, M., D’Silva, V., Griggio, A., Haller, L. and Kroening, D. (2013). Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL.
  • Seghir, M.N. and Brain, M. (2013). Simplifying the Verification of Quantified Array Assertions via Code Transformation.
  • Brain, M., D’Silva, V., Haller, L., Griggio, A. and Kroening, D. (2013). An Abstract Interpretation of DPLL(T).
  • Haller, L., Griggio, A., Brain, M., Kroening, D. and IEEE, (2012). Deciding Floating-Point Logic with Systematic Abstraction.
  • Yamaguchi, T., Brain, M., Ryder, C., Imai, Y., Kawamura, Y. and NYX BRAIN, M. Application of Abstract Interpretation to the Automotive Electronic Control System. Verification, Model Checking, and Abstract Interpretation.
  • Brain, M., Schanda, F. and SUN, Y. Building Better Bit-Blasting for Floating-Point Problems. International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Journal articles (3)

  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T. and Bienmüller, T. (2017). Incremental bounded model checking for embedded software. Formal Aspects of Computing, 29(5), pp. 911–931. doi:10.1007/s00165-017-0419-1.
  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B. … Sturm, T. (2016). Satisfiability Checking and Symbolic Computation. CoRR, abs/1607.06945.
  • Brain, M., D’Silva, V., Griggio, A., Haller, L. and Kroening, D. (2014). Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design, 45(2), pp. 213–245. doi:10.1007/s10703-013-0203-7.

Other (3)

  • Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B. … Sturm, T. (2017). Satisfiability checking and symbolic computation.
  • Brain, M., Joshi, S., Kroening, D. and Schrammel, P. Safety Verification and Refutation by k-invariants and k-induction (extended version).

    [publisher’s website]

  • Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T. and Bienmüller, T. Incremental Bounded Model Checking for Embedded Software (extended version).

    [publisher’s website]