Alberto Griggio

Angelo Susi

Proceedings of the Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, 2022

A comprehensive framework for the analysis of automotive systems.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, 2022

Analysis of Cyclic Fault Propagation via ASP.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2022

COMPASTA: Extending TASTE with Formal Design and Verification Functionality.

[BibT_eX]

[DOI]

Proceedings of the Model-Based Safety and Assessment - 8th International Symposium, 2022

Verification of SMT Systems with Quantifiers.

[BibT_eX]

[DOI]

Gianluca Redondi

Proceedings of the Automated Technology for Verification and Analysis, 2022

Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2022

2021

Certifying proofs for SAT-based model checking.

[BibT_eX]

[DOI]

Stefano Tonetta

Formal Methods Syst. Des., 2021

Proving the Existence of Fair Paths in Infinite-State Systems.

[BibT_eX]

[DOI]

Enrico Magnago

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

Optimization Modulo Non-linear Arithmetic via Incremental Linearization.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Efficient SMT-Based Analysis of Failure Propagation.

[BibT_eX]

[DOI]

Marco Bozzano

Anthony Fernandes Pires

Martin Jonás

Greg Kimberly

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning.

[BibT_eX]

[DOI]

Gianluca Redondi

Proceedings of the Automated Deduction - CADE 28, 2021

Automatic Discovery of Fair Paths in Infinite-State Transition Systems.

[BibT_eX]

[DOI]

Enrico Magnago

Proceedings of the Automated Technology for Verification and Analysis, 2021

2020

Symbolic computation and satisfiability checking.

[BibT_eX]

[DOI]

J. Symb. Comput., 2020

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators.

[BibT_eX]

[DOI]

Inf. Comput., 2020

Safe Decomposition of Startup Requirements: Verification and Synthesis.

[BibT_eX]

[DOI]

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

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Applications, 2020

2019

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization.

[BibT_eX]

[DOI]

Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2019

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.

[BibT_eX]

[DOI]

Muhammad Syifa'ul Mufid

Idriss Riouak

Stefano Tonetta

Enea Zaffanella

Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties.

[BibT_eX]

[DOI]

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

2018

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2018

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions.

[BibT_eX]

[DOI]

Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

Symbolic execution with existential second-order constraints.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Certifying Proofs for LTL Model Checking.

[BibT_eX]

[DOI]

Stefano Tonetta

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

Preface to special issue on satisfiability modulo theories.

[BibT_eX]

[DOI]

Philipp Rümmer

Formal Methods Syst. Des., 2017

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF.

[BibT_eX]

[DOI]

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

Benchmarking Solvers, SAT-style.

[BibT_eX]

[DOI]

Martin Brain

James H. Davenport

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

Satisfiability Modulo Transcendental Functions via Incremental Linearization.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

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

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

2016

Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2016

Infinite-state invariant checking with IC3 and predicate abstraction.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Satisfiability Checking meets Symbolic Computation (Project Paper).

[BibT_eX]

[DOI]

CoRR, 2016

Satisfiability checking and symbolic computation.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2016

The xSAP Safety Analysis Platform.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

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

Verilog2SMV: A tool for word-level verification.

[BibT_eX]

[DOI]

Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

HyComp: An SMT-Based Model Checker for Hybrid Systems.

[BibT_eX]

[DOI]

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

Parameter Synthesis with IC3 (Informal Presentation).

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Efficient Anytime Techniques for Model-Based Safety Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Deciding floating-point logic with abstract conflict driven clause learning.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

IC3 Modulo Theories via Implicit Predicate Abstraction.

[BibT_eX]

[DOI]

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

Towards Pareto-optimal parameter synthesis for monotonic cost functions.

[BibT_eX]

[DOI]

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

Verifying LTL Properties of Hybrid Systems with K-Liveness.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

The nuXmv Symbolic Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

An Abstract Interpretation of DPLL(T).

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

The MathSAT5 SMT Solver.

[BibT_eX]

[DOI]

Bastiaan Joost Schaafsma

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

A Modular Approach to MaxSAT Modulo Theories.

[BibT_eX]

[DOI]

Bastiaan Joost Schaafsma

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

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

[BibT_eX]

[DOI]

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

Parameter synthesis with IC3.

[BibT_eX]

[DOI]

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

2012

A Practical Approach to Satisability Modulo Linear Integer Arithmetic.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2012

Deciding floating-point logic with systematic abstraction.

[BibT_eX]

[DOI]

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

Software Model Checking via IC3.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Optimizing Monitoring Requirements in Self-adaptive Systems.

[BibT_eX]

[DOI]

Proceedings of the Enterprise, Business-Process and Information Systems Modeling, 2012

The 2012 SMT Competition.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

Broadening the Scope of SMT-COMP: the Application Track.

[BibT_eX]

[DOI]

Roberto Bruttomesso

Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012

2011

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2011

Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Effective word-level interpolation for software verification.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Kratos - A Software Model Checker for SystemC.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Efficient generation of craig interpolants in satisfiability modulo theories.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2010

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

[BibT_eX]

[DOI]

Thi Thieu Hoa Le

Log. Methods Comput. Sci., 2010

Satisfiability Modulo the Theory of Costs: Foundations and Applications.

[BibT_eX]

[DOI]

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

Tighter integration of BDDs and SMT for Predicate Abstraction.

[BibT_eX]

[DOI]

Anders Franzén

Krishnamani Kalyanasundaram

Proceedings of the Design, Automation and Test in Europe, 2010

2009

An Effective SMT Engine for Formal Verification.

[BibT_eX]

[DOI]

PhD thesis, 2009

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

Software model checking via large-block encoding.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Interpolant Generation for UTVPI.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Efficient Interpolant Generation in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

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

The MathSAT 4SMT Solver.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.

[BibT_eX]

[DOI]