Contact details
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
Conference papers and proceedings (31)
- Howe, J.M., Brain, M. and Gàmez-Montolio, A. (2025). Evaluating Binary Polynomials using Subpolynomials. SMT 2025: 23rd International Workshop on Satisfiability Modulo Theories 10-11 August, Glasgow, UK.
- Barlik, M. and Brain, M. (2025). Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2. SMT 2025: 23rd International Workshop on Satisfiability Modulo Theories 10-11 August, Glasgow, UK.
- Brain, M. and Polgreen, E. A Pyramid Of (Formal) Software Verification. .doi:10.1007/978-3-031-71177-0_24
- Brain, M. and Malkawi, M. (2024). Misconceptions about Loops in C. SOAP '24: 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis 25 June-, Copenhagen, Denmark.doi:10.1145/3652588.3663324
- Gàmez-Montolio, A., Florit, E., Brain, M. and Howe, J.M. Efficient Normalized Reduction and Generation of Equivalent Multivariate Binary Polynomials. Workshop on Binary Analysis Research.doi:10.14722/bar.2024.23014
- Howe, J. and Nyx Brain, M. (2023). Widening for Systems of Two Variables Per Inequality. 8th SC-Square Workshop 28 July-, Tromsø, Norway.
- Brain, M., Cid, C., Player, R. and Robson, W. Verifying Classic McEliece: Examining the Role of Formal Methods in Post-Quantum Cryptography Standardisation. .doi:10.1007/978-3-031-29689-5_2
- Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M.... Zohar, Y. cvc5: A Versatile and Industrial-Strength SMT Solver. .doi:10.1007/978-3-030-99524-9_24
- Brain, M. (2021). Further steps down the wrong path: Improving the bit-blasting of multiplication. 19th International Workshop on Satisfiability Modulo Theories 18-19 July, Online.
- Brain, M., Schanda, F. and Sun, Y. Building Better Bit-Blasting for Floating-Point Problems. .doi:10.1007/978-3-030-17462-0_5
- Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C. and Tinelli, C. Invertibility Conditions for Floating-Point Formulas. .doi:10.1007/978-3-030-25543-5_8
- 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.doi:10.1109/iceccs.2017.18
- Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Cimatti, A.... Traytel, D. SC-square: when Satisfiability Checking and Symbolic Computation join forces. .
- Sun, Y., Brain, M., Kroening, D., Hawthorn, A., Wilson, T., Schanda, F.... Broster, I. Functional Requirements-Based Automated Testing for Avionics. .doi:10.1109/ICECCS.2017.18
- Brain, M., Kroening, D. and McCleeary, R. Algebraic techniques in software verification : Challenges and opportunities. .
- Neville, D., Malton, A., Brain, M. and Kroening, D. Towards automated bounded model checking of API implementations. .
- Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B.... Sturm, T. SC2: Satisfiability checking meets symbolic computation (Project Paper). .doi:10.1007/978-3-319-42547-4_3
- Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B.... Sturm, T. $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation. .doi:10.1007/978-3-319-42547-4_3
- Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B.... Tompa, F.W. SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). .
- Brain, M., Hadarean, L., Kroening, D. and Martins, R. Automatic Generation of Propagation Complete SAT Encodings. .doi:10.1007/978-3-662-49122-5_26
- Brain, M., Joshi, S., Kroening, D. and Schrammel, P. Safety Verification and Refutation by k-invariants and k-induction. Static Analysis.doi:10.1007/978-3-662-49122-5_26
- 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.doi:10.1109/arith.2015.26
- Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T. and Bienmüller, T. Successful Use of Incremental BMC in the Automotive Industry. .doi:10.1007/978-3-319-19458-5_5
- Brain, M., Joshi, S., Kroening, D. and Schrammel, P. Safety Verification and Refutation by k-Invariants and k-Induction. .doi:10.1007/978-3-662-48288-9_9
- Brain, M., David, C., Kroening, D. and Schrammel, P. Model and Proof Generation for Heap-Manipulating Programs. .
- Brain, M., D’Silva, V., Griggio, A., Haller, L. and Kroening, D. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. .
- Seghir, M.N. and Brain, M. Simplifying the Verification of Quantified Array Assertions via Code Transformation. .doi:10.1007/978-3-642-38197-3_13
- Brain, M., D’Silva, V., Haller, L., Griggio, A. and Kroening, D. An Abstract Interpretation of DPLL(T). .
- Haller, L., Griggio, A., Brain, M., Kroening, D. and IEEE, 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.doi:10.1007/978-3-030-11245-5_20
- 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 (5)
- Brain, M. and Howe, J.M. (2026). Canonical Forms and Widening for Two Variables Per Inequality Systems. Mathematics in Computer Science, 20(1). doi:10.1007/s11786-025-00612-6
- 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. (2017). Satisfiability checking and symbolic computation. ACM Communications in Computer Algebra, 50(4), pp. 145-147. doi:10.1145/3055282.3055285
- Á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 (2)
- Brain, M., Joshi, S., Kroening, D. and Schrammel, P. Safety Verification and Refutation by k-invariants and k-induction (extended version).
- Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T. and Bienmüller, T. Incremental Bounded Model Checking for Embedded Software (extended version).