# Alessandro Cimatti

According to our database1, Alessandro Cimatti authored at least 213 papers between 1992 and 2020.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

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

Computation of the Transient in Max-Plus Linear Systems via SMT-Solving.
CoRR, 2020

Safe Decomposition of Startup Requirements: Verification and Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Temporal Planning with Intermediate Conditions and Effects.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019
Formal reliability analysis of redundancy architectures.
Formal Asp. Comput., 2019

Towards Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans.
CoRR, 2019

COMPASS 3.0.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2019

NuRV: A nuXmv Extension for Runtime Verification.
Proceedings of the Runtime Verification - 19th International Conference, 2019

Assumption-Based Runtime Verification with Partial Observability and Resets.
Proceedings of the Runtime Verification - 19th International Conference, 2019

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
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.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Robustness Envelopes for Temporal Plans.
Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions.
ACM Trans. Comput. Log., 2018

Tightening the contract refinements of a system architecture.
Formal Methods Syst. Des., 2018

Strong temporal planning with uncontrollable durations.
Artif. Intell., 2018

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions.
Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

Symbolic execution with existential second-order constraints.
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.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides.
Proceedings of the International Workshop on MILS: Architecture and Assurance for Secure Systems, 2018

Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Formal Specification and Verification of Dynamic Parametrized Architectures.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

2017
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study.
Proceedings of the Model-Based Safety and Assessment - 5th International Symposium, 2017

SMT-based analysis of switching multi-domain linear Kirchhoff networks.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Satisfiability Modulo Transcendental Functions via Incremental Linearization.
Proceedings of the Automated Deduction - CADE 26, 2017

SC-square: when Satisfiability Checking and Symbolic Computation join forces.
Proceedings of the ARCADE 2017, 2017

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic.
Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017

2016
Infinite-state invariant checking with IC3 and predicate abstraction.
Formal Methods Syst. Des., 2016

Satisfiability Checking meets Symbolic Computation (Project Paper).
CoRR, 2016

Satisfiability checking and symbolic computation.
ACM Commun. Comput. Algebra, 2016

Dynamic controllability via Timed Game Automata.
Acta Informatica, 2016

The xSAP Safety Analysis Platform.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Tightening a Contract Refinement.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

SC<sup>2</sup>: Satisfiability Checking Meets Symbolic Computation - (Project Paper).
Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Automated Synthesis of Timed Failure Propagation Graphs.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

From Electrical Switched Networks to Hybrid Automata.
Proceedings of the FM 2016: Formal Methods, 2016

Model-Based Design of an Energy-System Embedded Controller Using Taste.
Proceedings of the FM 2016: Formal Methods, 2016

Verilog2SMV: A tool for word-level verification.
Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

A Lazy Approach to Temporal Epistemic Logic Model Checking.
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

Automated Verification and Tightening of Failure Propagation Models.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

2015
Contracts-refinement proof system for component-based embedded systems.
Sci. Comput. Program., 2015

Safety assessment of AltaRica models via symbolic model checking.
Sci. Comput. Program., 2015

HRELTL: A temporal logic for hybrid systems.
Inf. Comput., 2015

Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic.
Log. Methods Comput. Sci., 2015

Solving strong controllability of temporal problems with uncertainty using SMT.
Constraints An Int. J., 2015

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty.
Artif. Intell., 2015

HyComp: An SMT-Based Model Checker for Hybrid Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Parameter Synthesis with IC3 (Informal Presentation).
Proceedings of the 2nd International Workshop on Synthesis of Complex Parameters, 2015

Combining MILS with Contract-Based Design for Safety and Security Requirements.
Proceedings of the Computer Safety, Reliability, and Security, 2015

Comparing Different Functional Allocations in Automated Air Traffic Control Design.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Formal Design and Safety Analysis of AIR6110 Wheel Brake System.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Efficient Anytime Techniques for Model-Based Safety Analysis.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Formal Verification of Infinite-State BIP Models.
Proceedings of the Automated Technology for Verification and Analysis, 2015

Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach.
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

SMT-Based Validation of Timed Failure Propagation Graphs.
Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014
Spacecraft early design validation using formal methods.
Reliab. Eng. Syst. Saf., 2014

Quantifier-free encoding of invariants for hybrid systems.
Formal Methods Syst. Des., 2014

Automated Planning and Model Checking (Dagstuhl Seminar 14482).
Dagstuhl Reports, 2014

Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation.
Proceedings of the 21st International Symposium on Temporal Representation and Reasoning, 2014

IC3 Modulo Theories via Implicit Predicate Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Proceedings of the Model-Based Safety and Assessment - 4th International Symposium, 2014

Towards Pareto-optimal parameter synthesis for monotonic cost functions.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Verifying LTL Properties of Hybrid Systems with K-Liveness.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

The nuXmv Symbolic Model Checker.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Formal Safety Assessment via Contract-Based Design.
Proceedings of the Automated Technology for Verification and Analysis, 2014

Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty.
Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013
Software Model Checking SystemC.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2013

SMT-based scenario verification for hybrid systems.
Formal Methods Syst. Des., 2013

The MathSAT5 SMT Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

A Modular Approach to MaxSAT Modulo Theories.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

OCRA: A tool for checking the refinement of temporal contracts.
Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Automated Analysis of Reliability Architectures.
Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013

Efficient Analysis of Reliability Architectures via Predicate Abstraction.
Proceedings of the Hardware and Software: Verification and Testing, 2013

Parameter synthesis with IC3.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Time-aware relational abstractions for hybrid systems.
Proceedings of the International Conference on Embedded Software, 2013

SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads.
Proceedings of the Automated Technology for Verification and Analysis, 2013

Timelines with Temporal Uncertainty.
Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, 2013

A Formal Framework for the Specification, Verification and Synthesis of Diagnosers.
Proceedings of the Late-Breaking Developments in the Field of Artificial Intelligence, 2013

2012
Validation of requirements for hybrid systems: A formal approach.
ACM Trans. Softw. Eng. Methodol., 2012

Software Model Checking with Explicit Scheduler and Symbolic Threads
Log. Methods Comput. Sci., 2012

Verification of parametric system designs.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

A quantifier-free SMT encoding of non-linear hybrid automata.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Application of SMT solvers to hybrid system verification.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

A Property-Based Proof System for Contract-Based Design.
Proceedings of the 38th Euromicro Conference on Software Engineering and Advanced Applications, 2012

Solving Temporal Problems Using SMT: Strong Controllability.
Proceedings of the Principles and Practice of Constraint Programming, 2012

Software Model Checking via IC3.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

SMT-Based Verification of Hybrid Systems.
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

Solving Temporal Problems Using SMT: Weak Controllability.
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

Symbolic Synthesis of Observability Requirements for Diagnosability.
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

2011
Formalizing requirements with object models and temporal constraints.
Software and Systems Modeling, 2011

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.
J. Artif. Intell. Res., 2011

Symbolic Model Checking and Safety Assessment of Altarica models.
ECEASST, 2011

Safety, Dependability and Performance Analysis of Extended AADL Models.
Comput. J., 2011

Boosting Lazy Abstraction for SystemC with Partial Order Reduction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

An Analytic Evaluation of SystemC Encodings in Promela.
Proceedings of the Model Checking Software, 2011

A Comprehensive Approach to On-Board Autonomy Verification and Validation.
Proceedings of the IJCAI 2011, 2011

OthelloPlay: a plug-in based tool for requirement formalization and validation.
Proceedings of the 1st Workshop on Developing Tools as Plug-ins, 2011

Proving and explaining the unfeasibility of message sequence charts for hybrid systems.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction.
Proceedings of the 37th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2011, Oulu, Finland, August 30, 2011

Efficient Scenario Verification for Hybrid Automata.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Kratos - A Software Model Checker for SystemC.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Efficient generation of craig interpolants in satisfiability modulo theories.
ACM Trans. Comput. Log., 2010

From Sequential Extended Regular Expressions to NFA with Symbolic Labels.
Proceedings of the Implementation and Application of Automata, 2010

Satisfiability Modulo the Theory of Costs: Foundations and Applications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

SMT-Based Software Model Checking.
Proceedings of the Model Checking Software, 2010

Formalization and validation of a subset of the European Train Control System.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Model Checking of Hybrid Systems Using Shallow Synchronization.
Proceedings of the Formal Techniques for Distributed Systems, 2010

Applying SMT in symbolic execution of microcode.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Verifying SystemC: A software model checking approach.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Parametric analysis of distributed firm real-time systems: A case study.
Proceedings of 15th IEEE International Conference on Emerging Technologies and Factory Automation, 2010

Tighter integration of BDDs and SMT for Predicate Abstraction.
Proceedings of the Design, Automation and Test in Europe, 2010

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

RATSY - A New Requirements Analysis Tool with Synthesis.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Formalization and Validation of Safety-Critical Requirements
Proceedings of the Proceedings FM-09 Workshop on Formal Methods for Aerospace, 2009

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.
Ann. Math. Artif. Intell., 2009

Verification and performance evaluation of aadl models.
Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems.
Proceedings of the Computer Safety, 2009

Model-Based Codesign of Critical Embedded Systems.
Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems ( ACES-MB 2009 ), 2009

Codesign of dependable systems: A component-based modeling language.
Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Supporting Requirements Validation: The EuRailCheck Tool.
Proceedings of the ASE 2009, 2009

Structure-aware computation of predicate abstraction.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Software model checking via large-block encoding.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Requirements Validation for Hybrid Systems.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Interpolant Generation for UTVPI.
Proceedings of the Automated Deduction, 2009

2008
Automated Planning.
Proceedings of the Handbook of Knowledge Representation, 2008

Symbolic Compilation of PSL.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2008

Diagnostic Information for Realizability.
Proceedings of the Verification, 2008

Efficient Interpolant Generation in Satisfiability Modulo Theories.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Object Models with Temporal Constraints.
Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

Symbolic Computation of Schedulability Regions Using Parametric Timed Automata.
Proceedings of the 29th IEEE Real-Time Systems Symposium, 2008

From Informal Requirements to Property-Driven Formal Validation.
Proceedings of the Formal Methods for Industrial Critical Systems, 2008

The MathSAT 4SMT Solver.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Symbolic Implementation of Alternating Automata.
Int. J. Found. Comput. Sci., 2007

Syntactic Optimizations for PSL Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Boolean Abstraction for Temporal Logic Satisfiability.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Verifying Heap-Manipulating Programs in an SMT Framework.
Proceedings of the Automated Technology for Verification and Analysis, 2007

Symbolic Fault Tree Analysis for Reactive Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2007

2006
Efficient theory combination via boolean search.
Inf. Comput., 2006

Encoding RTL Constructs for MathSAT: a Preliminary Report.
Electron. Notes Theor. Comput. Sci., 2006

Preface.
Electron. Notes Theor. Comput. Sci., 2006

Strong planning under partial observability.
Artif. Intell., 2006

Symbolic Implementation of Alternating Automata.
Proceedings of the Implementation and Application of Automata, 2006

Building Efficient Decision Procedures on Top of SAT Solvers.
Proceedings of the Formal Methods for Hardware Verification, 2006

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis.
Proceedings of the Model Checking and Artificial Intelligence, 4th Workshop, 2006

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in <i>SMT</i>(<i>EUF</i> È<i>T</i>).
Proceedings of the Logic for Programming, 2006

From PSL to NBA: a Modular Symbolic Encoding.
Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Stong Cyclic Planning Under Partial Observability.
Proceedings of the ECAI 2006, 17th European Conference on Artificial Intelligence, August 29, 2006

Formal analysis of hardware requirements.
Proceedings of the 43rd Design Automation Conference, 2006

Towards Strong Cyclic Planning under Partial Observability.
Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling, 2006

2005
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.
J. Autom. Reasoning, 2005

Verifying Industrial Hybrid Systems with MathSAT.
Electron. Notes Theor. Comput. Sci., 2005

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The MathSAT 3 System.
Proceedings of the Automated Deduction, 2005

2004
Conformant planning via symbolic model checking and heuristic search.
Artif. Intell., 2004

Bounded Verification of Past LTL.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems.
Proceedings of the 16th Eureopean Conference on Artificial Intelligence, 2004

Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains.
Proceedings of the 16th Eureopean Conference on Artificial Intelligence, 2004

2003
Weak, strong, and strong cyclic planning via symbolic model checking.
Artif. Intell., 2003

Bounded model checking.

Bounded Model Checking for Past LTL.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Formal Verification of Diagnosability via Symbolic Model Checking.
Proceedings of the IJCAI-03, 2003

A Framework for Planning with Extended Goals under Partial Observability.
Proceedings of the Thirteenth International Conference on Automated Planning and Scheduling (ICAPS 2003), 2003

2002
Improving the Encoding of LTL Model Checking into SAT.
Proceedings of the Verification, 2002

Integrating BDD-Based and SAT-Based Symbolic Model Checking.
Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

Bounded Model Checking for Timed Systems.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2002

Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking.
Proceedings of the 15th Eureopean Conference on Artificial Intelligence, 2002

NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.
Proceedings of the Automated Deduction, 2002

Validation of Multiagent Systems by Symbolic Model Checking.
Proceedings of the Agent-Oriented Software Engineering III, Third International Workshop, 2002

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements.
Proceedings of the Artificial Intelligence, 2002

Improving Heuristics for Planning as Search in Belief Space.
Proceedings of the Sixth International Conference on Artificial Intelligence Planning Systems, 2002

2001
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking.
Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning.
Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

2000
NUSMV: A New Symbolic Model Checker.
Int. J. Softw. Tools Technol. Transf., 2000

Verification of a safety-critical railway interlocking system with real-time constraints.
Sci. Comput. Program., 2000

Conformant Planning via Symbolic Model Checking.
J. Artif. Intell. Res., 2000

Industrial Applications of Model Checking.
Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

1999
Preface.
Electron. Notes Theor. Comput. Sci., 1999

Symbolic Model Checking without BDDs.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Formal Specification and Development of a Safety-Critical Train Management System.
Proceedings of the Computer Safety, 1999

Formal Specification and Validation of a Vital Communication Protocol.
Proceedings of the FM'99 - Formal Methods, 1999

Conformant Planning via Model Checking.
Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Symbolic Model Checking Using SAT Procedures instead of BDDs.
Proceedings of the 36th Conference on Design Automation, 1999

NUSMV: A New Symbolic Model Verifier.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Formal Verification of a Railway Interlocking System using Model Checking.
Formal Asp. Comput., 1998

A Many-Sorted Natural Deduction.
Comput. Intell., 1998

Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System.
Proceedings of the Computer Safety, 1998

A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools.
Proceedings of the Computer Safety, 1998

Strong Planning in Non-Deterministic Domains Via Model Checking.
Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, 1998

Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains.
Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, 1998

1997
Planning via Model Checking: A Decision Procedure for <i>AR</i>.
Proceedings of the Recent Advances in AI Planning, 4th European Conference on Planning, 1997

A Provably Correct Embedded Verifier for the Certification of Safety Critical Software.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996
Visual representation of natural language scene descriptions.
IEEE Trans. Syst. Man Cybern. Part B, 1996

Computational reflection via mechanized logical deduction.
Int. J. Intell. Syst., 1996

Mechanizing Multi-Agent Reasoning with Belief Contexts.
Proceedings of the Practical Reasoning, 1996

Formal Specification of Beliefs in Multi-Agent Systems.
Proceedings of the Intelligent Agents III, 1996

1995
Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance.
Proceedings of the First International Conference on Multiagent Systems, 1995

1994
MRG: Building planers for real-world complex applications.
Applied Artificial Intelligence, 1994

Introspective Metatheoretic Reasoning.
Proceedings of the Logic Programming Synthesis and Transformation, 1994

Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study.
Proceedings of the Intelligent Agents, 1994

1993
Building and Executing Proof Strategies in a Formal Metatheory.
Proceedings of the Advances in Artificial Intelligence, 1993

1992
Beyond the Single Planning Paradigm: Introspective Planning.
Proceedings of the 10th European Conference on Artificial Intelligence, 1992