Filtros de búsqueda

Lista de obras de Alessandro Cimatti

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

artículo científico publicado en 2016

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

A Many-Sorted Natural Deduction

artículo científico publicado en 1998

A Model Checker for AADL

artículo científico publicado en 2010

A Modular Approach to MaxSAT Modulo Theories

artículo científico publicado en 2013

A Property-Based Proof System for Contract-Based Design

artículo científico publicado en 2012

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

artículo científico publicado en 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

artículo científico publicado en 1998

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

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

artículo científico publicado en 1997

An Analytic Evaluation of SystemC Encodings in Promela

artículo científico publicado en 2011

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

artículo científico publicado en 2005

An Integrated Process for FDIR Design in Aerospace

artículo científico publicado en 2014

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

artículo científico publicado en 2015

Automated Analysis of Reliability Architectures

artículo científico publicado en 2013

Beyond Boolean SAT: Satisfiability modulo theories

artículo científico publicado en 2008

Boolean Abstraction for Temporal Logic Satisfiability

Boosting Lazy Abstraction for SystemC with Partial Order Reduction

artículo científico publicado en 2011

Bounded Model Checking

artículo científico publicado en 2003

Bounded Model Checking for Past LTL

artículo científico publicado en 2003

Bounded Model Checking for Timed Systems

artículo científico publicado en 2002

Bounded Verification of Past LTL

artículo científico publicado en 2004

Building Efficient Decision Procedures on Top of SAT Solvers

artículo científico publicado en 2006

Building and executing proof strategies in a formal metatheory

artículo científico publicado en 1993

Chapter 22 Automated Planning

artículo científico publicado en 2008

Codesign of dependable systems: A component-based modeling language

artículo científico publicado en 2009

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

artículo científico publicado en 2015

Comparing different functional allocations in automated air traffic control design

artículo científico publicado en 2015

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers

artículo científico publicado en 2007

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories

artículo científico publicado en 2011

Conformant Planning via Model Checking

artículo científico publicado en 2000

Conformant Planning via Symbolic Model Checking

artículo científico publicado en 2000

Conformant planning via symbolic model checking and heuristic search

artículo científico publicado en 2004

Contracts-refinement proof system for component-based embedded systems

artículo científico publicado en 2015

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

artículo científico publicado en 2006

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

artículo científico publicado en 2009

Diagnostic Information for Realizability

Dynamic controllability via Timed Game Automata

artículo científico publicado en 2016

Efficient Analysis of Reliability Architectures via Predicate Abstraction

artículo científico publicado en 2013

Efficient Anytime Techniques for Model-Based Safety Analysis

artículo científico publicado en 2015

Efficient Interpolant Generation in Satisfiability Modulo Theories

Efficient Satisfiability Modulo Theories via Delayed Theory Combination

artículo científico publicado en 2005

Efficient Scenario Verification for Hybrid Automata

artículo científico publicado en 2011

Efficient generation of craig interpolants in satisfiability modulo theories

artículo científico publicado en 2010

Efficient theory combination via boolean search

artículo científico publicado en 2006

Encoding RTL Constructs for MathSAT: a Preliminary Report

artículo científico publicado en 2006

Flexible planning by integrating multilevel reasoning

artículo científico publicado en 1995

Formal Design and Safety Analysis of AIR6110 Wheel Brake System

artículo científico publicado en 2015

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

artículo científico publicado en 2015

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

artículo científico publicado en 2014

Formal Safety Assessment via Contract-Based Design

artículo científico publicado en 2014

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

artículo científico publicado en 1999

Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System

artículo científico publicado en 2012

Formal Verification of Infinite-State BIP Models

artículo científico publicado en 2015

Formal Verification of a Railway Interlocking System using Model Checking

artículo científico publicado en 1998

Formal analysis of hardware requirements

artículo científico publicado en 2006

Formal specification and validation of a vital communication protocol

artículo científico publicado en 1999

Formal specification of beliefs in multi-agent systems

artículo científico publicado en 1997

Formalization and Validation of Safety-Critical Requirements

artículo científico publicado en 2010

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

artículo científico publicado en 2010

Formalizing requirements with object models and temporal constraints

artículo científico publicado en 2009

From Electrical Switched Networks to Hybrid Automata

artículo científico publicado en 2016

From Informal Requirements to Property-Driven Formal Validation

artículo científico publicado en 2009

From PSL to NBA: a Modular Symbolic Encoding

artículo científico publicado en 2006

From Sequential Extended Regular Expressions to NFA with Symbolic Labels

artículo científico publicado en 2011

HRELTL: A temporal logic for hybrid systems

artículo científico publicado en 2015

HyComp: An SMT-Based Model Checker for Hybrid Systems

artículo científico publicado en 2015

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction

artículo científico publicado en 2011

IC3 Modulo Theories via Implicit Predicate Abstraction

artículo científico publicado en 2014

Improving the Encoding of LTL Model Checking into SAT

artículo científico publicado en 2002

Industrial Applications of Model Checking

artículo científico publicado en 2001

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

artículo científico publicado en 2016

Infinite-state invariant checking with IC3 and predicate abstraction

artículo científico publicado en 2016

Integrating BDD-Based and SAT-Based Symbolic Model Checking

artículo científico publicado en 2002

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

artículo científico publicado en 2002

Interpolant Generation for UTVPI

artículo científico publicado en 2009

Introspective metatheoretic reasoning

artículo científico publicado en 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

artículo científico publicado en 2017

Kratos – A Software Model Checker for SystemC

artículo científico publicado en 2011

MRG: BUILDING PLANNERS FOR REAL-WORLD COMPLEX APPLICATIONS

artículo científico publicado en 1994

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

artículo científico publicado en 2005

Mechanizing multi-agent reasoning with belief contexts

artículo científico publicado en 1996

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

artículo científico publicado en 1998

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

artículo científico publicado en 2016

Model Checking of Hybrid Systems Using Shallow Synchronization

artículo científico publicado en 2010

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

artículo científico publicado en 2016

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

artículo científico publicado en 1995

NUSMV: a new symbolic model checker

artículo científico publicado en 2000

NuSMV 2: An OpenSource Tool for Symbolic Model Checking

artículo científico publicado en 2002

NuSMV: A New Symbolic Model Verifier

artículo científico publicado en 1999

OCRA: A tool for checking the refinement of temporal contracts

artículo científico publicado en 2013

Object Models with Temporal Constraints

artículo científico publicado en 2008

OthelloPlay

artículo científico publicado en 2011

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

artículo científico publicado en 2010

Planning via model checking: A decision procedure for AR

artículo científico publicado en 1997

Preface

artículo científico publicado en 2006

Preface

artículo científico publicado en 2001

Quantifier-free encoding of invariants for hybrid systems

artículo científico publicado en 2013

RATSY – A New Requirements Analysis Tool with Synthesis

artículo científico publicado en 2010

Requirements Validation for Hybrid Systems

artículo científico publicado en 2009

SMT-Based Software Model Checking

artículo científico publicado en 2013

SMT-Based Software Model Checking

artículo científico publicado en 2010

SMT-based scenario verification for hybrid systems

artículo científico publicado en 2012

SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA

artículo científico publicado en 2007

Safety assessment of AltaRica models via symbolic model checking

artículo científico publicado en 2015

Safety, Dependability and Performance Analysis of Extended AADL Models

artículo científico publicado en 2010

Satisfiability Modulo Transcendental Functions via Incremental Linearization

artículo científico publicado en 2017

Satisfiability Modulo the Theory of Costs: Foundations and Applications

artículo científico publicado en 2010

Satisfiability checking and symbolic computation

artículo científico publicado en 2017

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

artículo científico publicado en 2001

Software Model Checking SystemC

artículo científico publicado en 2013

Software Model Checking via IC3

artículo científico publicado en 2012

Software Model Checking with Explicit Scheduler and Symbolic Threads

artículo científico publicado en 2012

Software model checking via large-block encoding

artículo científico publicado en 2009

Solving Temporal Problems Using SMT: Strong Controllability

artículo científico publicado en 2012

Solving strong controllability of temporal problems with uncertainty using SMT

artículo científico publicado en 2014

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

artículo científico publicado en 2014

Spacecraft early design validation using formal methods

artículo científico publicado en 2014

Strong planning under partial observability

artículo científico publicado en 2006

Strong temporal planning with uncontrollable durations

artículo científico publicado en 2018

Structure-aware computation of predicate abstraction

artículo científico publicado en 2009

Supporting Requirements Validation: The EuRailCheck Tool

artículo científico publicado en 2009

Symbolic Compilation of PSL

artículo científico publicado en 2008

Symbolic Computation of Schedulability Regions Using Parametric Timed Automata

artículo científico publicado en 2008

Symbolic Fault Tree Analysis for Reactive Systems

Symbolic Implementation of Alternating Automata

artículo científico publicado en 2006

Symbolic Model Checking without BDDs

artículo científico publicado en 1999

Symbolic model checking using SAT procedures instead of BDDs

artículo científico publicado en 1999

Syntactic Optimizations for PSL Verification

System-Software Co-Engineering: Dependability and Safety Perspective

artículo científico publicado en 2011

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

artículo científico publicado en 2009

The MathSAT 3 System

artículo científico publicado en 2005

The MathSAT 4 SMT Solver

The MathSAT5 SMT Solver

artículo científico publicado en 2013

The nuXmv Symbolic Model Checker

artículo científico publicado en 2014

The xSAP Safety Analysis Platform

artículo científico publicado en 2016

Tightening a Contract Refinement

artículo científico publicado en 2016

Tightening the contract refinements of a system architecture

artículo científico publicado en 2018

Time-aware relational abstractions for hybrid systems

artículo científico publicado en 2013

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

artículo científico publicado en 2017

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

artículo científico publicado en 2006

Towards Pareto-optimal parameter synthesis for monotonie cost functions

artículo científico publicado en 2014

Validation of Multiagent Systems by Symbolic Model Checking

artículo científico publicado en 2003

Validation of requirements for hybrid systems

artículo científico publicado en 2012

Verification and performance evaluation of aadl models

artículo científico publicado en 2009

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

artículo científico publicado en 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

artículo científico publicado en 2005

Verifying LTL Properties of Hybrid Systems with K-Liveness

artículo científico publicado en 2014

Visual representation of natural language scene descriptions

artículo científico publicado en 1996

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

artículo científico publicado en 2003