Search filters

Authors whose works are in public domain in at least one jurisdiction

List of works by Alessandro Cimatti

$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation

scientific article published in 2016

A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems

A Many-Sorted Natural Deduction

scientific article published in February 1998

A Model Checker for AADL

scientific article published in 2010

A Modular Approach to MaxSAT Modulo Theories

scientific article published in 2013

A Property-Based Proof System for Contract-Based Design

scientific article published in September 2012

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions

scientific article published in 2002

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

scholarly article

A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools

scientific article published in 1998

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis

A provably correct embedded verifier for the certification of safety critical software

scientific article published in 1997

An Analytic Evaluation of SystemC Encodings in Promela

scientific article published in 2011

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic

scientific article published in 2005

An Integrated Process for FDIR Design in Aerospace

scientific article published in 2014

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

scientific article published in July 2015

Automated Analysis of Reliability Architectures

scientific article published in July 2013

Beyond Boolean SAT: Satisfiability modulo theories

scientific article published in 2008

Boolean Abstraction for Temporal Logic Satisfiability

Boosting Lazy Abstraction for SystemC with Partial Order Reduction

scientific article published in 2011

Bounded Model Checking

scientific article published in 2003

Bounded Model Checking for Past LTL

scientific article published in 2003

Bounded Model Checking for Timed Systems

scientific article published in 2002

Bounded Verification of Past LTL

scientific article published in 2004

Building Efficient Decision Procedures on Top of SAT Solvers

scientific article published in 2006

Building and executing proof strategies in a formal metatheory

scientific article published in 1993

Chapter 22 Automated Planning

scientific article published in 2008

Codesign of dependable systems: A component-based modeling language

scientific article published in July 2009

Combining MILS with Contract-Based Design for Safety and Security Requirements

scientific article published in 2015

Comparing different functional allocations in automated air traffic control design

scientific article published in September 2015

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers

scientific article published in November 2007

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories

scientific article published on 14 April 2011

Conformant Planning via Model Checking

scientific article published in 2000

Conformant Planning via Symbolic Model Checking

scientific article published in December 2000

Conformant planning via symbolic model checking and heuristic search

scientific article published in November 2004

Contracts-refinement proof system for component-based embedded systems

scientific article published in January 2015

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis

scientific article published in 2006

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

scientific article published in February 2009

Diagnostic Information for Realizability

Dynamic controllability via Timed Game Automata

scientific article published in February 2016

Efficient Analysis of Reliability Architectures via Predicate Abstraction

scientific article published in 2013

Efficient Anytime Techniques for Model-Based Safety Analysis

scientific article published in 2015

Efficient Interpolant Generation in Satisfiability Modulo Theories

Efficient Satisfiability Modulo Theories via Delayed Theory Combination

scientific article published in 2005

Efficient Scenario Verification for Hybrid Automata

scientific article published in 2011

Efficient generation of craig interpolants in satisfiability modulo theories

scientific article published in October 2010

Efficient theory combination via boolean search

scientific article published in October 2006

Encoding RTL Constructs for MathSAT: a Preliminary Report

scientific article published in January 2006

Flexible planning by integrating multilevel reasoning

scientific article published in August 1995

Formal Design and Safety Analysis of AIR6110 Wheel Brake System

scientific article published in 2015

Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic

scientific article published on 4 November 2015

Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic

scientific article published in 2014

Formal Safety Assessment via Contract-Based Design

scientific article published in 2014

Formal Specification and Development of a Safety-Critical Train Management System

scientific article published in 1999

Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System

scientific article published in 2012

Formal Verification of Infinite-State BIP Models

scientific article published in 2015

Formal Verification of a Railway Interlocking System using Model Checking

scientific article published on 27 April 1998

Formal analysis of hardware requirements

scientific article published in 2006

Formal specification and validation of a vital communication protocol

scientific article published in 1999

Formal specification of beliefs in multi-agent systems

scientific article published in 1997

Formalization and Validation of Safety-Critical Requirements

scientific article published on 28 March 2010

Formalization and validation of a subset of the European Train Control System

scientific article published in 2010

Formalizing requirements with object models and temporal constraints

scientific article published on 19 August 2009

From Electrical Switched Networks to Hybrid Automata

scientific article published in 2016

From Informal Requirements to Property-Driven Formal Validation

scientific article published in 2009

From PSL to NBA: a Modular Symbolic Encoding

scientific article published in November 2006

From Sequential Extended Regular Expressions to NFA with Symbolic Labels

scientific article published in 2011

HRELTL: A temporal logic for hybrid systems

scientific article published in December 2015

HyComp: An SMT-Based Model Checker for Hybrid Systems

scientific article published in 2015

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction

scientific article published in August 2011

IC3 Modulo Theories via Implicit Predicate Abstraction

scientific article published in 2014

Improving the Encoding of LTL Model Checking into SAT

scientific article published in 2002

Industrial Applications of Model Checking

scientific article published in 2001

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

scientific article published in 2016

Infinite-state invariant checking with IC3 and predicate abstraction

scientific article published on 23 September 2016

Integrating BDD-Based and SAT-Based Symbolic Model Checking

scientific article published in 2002

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements

scientific article published in 2002

Interpolant Generation for UTVPI

scientific article published in 2009

Introspective metatheoretic reasoning

scientific article published in 1994

Invariant Checking for SMT-Based Systems with Quantifiers

scientific article published on 03 August 2024

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

scientific article published in 2017

Kratos – A Software Model Checker for SystemC

scientific article published in 2011

MRG: BUILDING PLANNERS FOR REAL-WORLD COMPLEX APPLICATIONS

scientific article published in July 1994

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

scientific article published in October 2005

Mechanizing multi-agent reasoning with belief contexts

scientific article published in 1996

Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System

scientific article published in 1998

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration

scientific article published in 2016

Model Checking of Hybrid Systems Using Shallow Synchronization

scientific article published in 2010

Model-Based Design of an Energy-System Embedded Controller Using Taste

scientific article published in 2016

Multi-agent reasoning with belief contexts: the approach and a case study

scientific article published in 1995

NUSMV: a new symbolic model checker

scientific article published in March 2000

NuSMV 2: An OpenSource Tool for Symbolic Model Checking

scientific article published in 2002

NuSMV: A New Symbolic Model Verifier

scientific article published in 1999

OCRA: A tool for checking the refinement of temporal contracts

scientific article published in November 2013

Object Models with Temporal Constraints

scientific article published in 2008

OthelloPlay

scientific article published in 2011

Parametric analysis of distributed firm real-time systems: A case study

scientific article published in September 2010

Planning via model checking: A decision procedure for AR

scientific article published in 1997

Preface

scientific article published in January 2006

Preface

scientific article published in December 2001

Quantifier-free encoding of invariants for hybrid systems

scientific article published on 7 December 2013

RATSY – A New Requirements Analysis Tool with Synthesis

scientific article published in 2010

Requirements Validation for Hybrid Systems

scientific article published in 2009

SMT-Based Software Model Checking

scientific article published in 2013

SMT-Based Software Model Checking

scientific article published in 2010

SMT-based scenario verification for hybrid systems

scientific article published on 16 May 2012

SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA

scientific article published in August 2007

Safety assessment of AltaRica models via symbolic model checking

scientific article published in February 2015

Safety, Dependability and Performance Analysis of Extended AADL Models

scientific article published on 17 March 2010

Satisfiability Modulo Transcendental Functions via Incremental Linearization

scientific article published in 2017

Satisfiability Modulo the Theory of Costs: Foundations and Applications

scientific article published in 2010

Satisfiability checking and symbolic computation

scientific article published on 22 February 2017

Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking

scientific article published in 2001

Software Model Checking SystemC

scientific article published in May 2013

Software Model Checking via IC3

scientific article published in 2012

Software Model Checking with Explicit Scheduler and Symbolic Threads

scientific article published on 5 August 2012

Software model checking via large-block encoding

scientific article published in November 2009

Solving Temporal Problems Using SMT: Strong Controllability

scientific article published in 2012

Solving strong controllability of temporal problems with uncertainty using SMT

scientific article published on 4 July 2014

Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation

scientific article published in September 2014

Spacecraft early design validation using formal methods

scientific article published in December 2014

Strong planning under partial observability

scientific article published in April 2006

Strong temporal planning with uncontrollable durations

scientific article published in March 2018

Structure-aware computation of predicate abstraction

scientific article published in November 2009

Supporting Requirements Validation: The EuRailCheck Tool

scientific article published in November 2009

Symbolic Compilation of PSL

scientific article published in October 2008

Symbolic Computation of Schedulability Regions Using Parametric Timed Automata

scientific article published in November 2008

Symbolic Fault Tree Analysis for Reactive Systems

Symbolic Implementation of Alternating Automata

scientific article published in 2006

Symbolic Model Checking without BDDs

scientific article published in 1999

Symbolic model checking using SAT procedures instead of BDDs

scientific article published in 1999

Syntactic Optimizations for PSL Verification

System-Software Co-Engineering: Dependability and Safety Perspective

scientific article published in August 2011

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems

scientific article published in 2009

The MathSAT 3 System

scientific article published in 2005

The MathSAT 4 SMT Solver

The MathSAT5 SMT Solver

scientific article published in 2013

The nuXmv Symbolic Model Checker

scientific article published in 2014

The xSAP Safety Analysis Platform

scientific article published in 2016

Tightening a Contract Refinement

scientific article published in 2016

Tightening the contract refinements of a system architecture

scientific article published on 3 January 2018

Time-aware relational abstractions for hybrid systems

scientific article published in September 2013

Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study

scientific article published in 2017

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

scientific article published in 2006

Towards Pareto-optimal parameter synthesis for monotonie cost functions

scientific article published in October 2014

Validation of Multiagent Systems by Symbolic Model Checking

scientific article published in 2003

Validation of requirements for hybrid systems

scientific article published in November 2012

Verification and performance evaluation of aadl models

scientific article published in 2009

Verification of a safety-critical railway interlocking system with real-time constraints

scientific article published in January 2000

Verification of a safety-critical railway interlocking system with real-time constraints

Verifying Heap-Manipulating Programs in an SMT Framework

Verifying Industrial Hybrid Systems with MathSAT

scientific article published in March 2005

Verifying LTL Properties of Hybrid Systems with K-Liveness

scientific article published in 2014

Visual representation of natural language scene descriptions

scientific article published in 1996

Weak, strong, and strong cyclic planning via symbolic model checking

scientific article published in July 2003