Alessandro Cimatti

Domenico Ernesto Garrubba

Angelo Susi

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

Formal Design and Validation of an Automatic Train Operation Control System.

[BibT_eX]

[DOI]

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 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

Symbolic Encoding of Reliability for the Design of Redundant Architectures.

[BibT_eX]

[DOI]

Proceedings of the 5th IEEE International Conference on Industrial Cyber-Physical Systems, 2022

A first-order logic characterisation of safety and co-safety languages.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2022

Abstraction Modulo Stability for Reverse Engineering.

[BibT_eX]

[DOI]

Anna Becchi

Proceedings of the Computer Aided Verification - 34th International Conference, 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

Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping.

[BibT_eX]

[DOI]

Stefan Panjkovic

Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

2021

A Comprehensive Approach to On-board Autonomy Verification and Validation.

[BibT_eX]

[DOI]

ACM Trans. Intell. Syst. Technol., 2021

Model-based Safety Assessment of a Triple Modular Generator with xSAP.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2021

Expressiveness of Extended Bounded Response LTL.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 12th International Symposium on Games, 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

Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans.

[BibT_eX]

[DOI]

Proceedings of the 28th International Symposium on Temporal Representation and Reasoning, 2021

Assumption-Based Runtime Verification of Infinite-State Systems.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 21st International Conference, 2021

Reverse engineering with P-stable Abstractions.

[BibT_eX]

[DOI]

Anna Becchi

Enea Zaffanella

Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, 2021

Optimization Modulo Non-linear Arithmetic via Incremental Linearization.

[BibT_eX]

[DOI]

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

SMT-Based Model Checking of Max-Plus Linear Systems.

[BibT_eX]

[DOI]

Muhammad Syifa'ul Mufid

Alessandro Abate

Proceedings of the 32nd International Conference on Concurrency Theory, 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]

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

Automatic Design Space Exploration of Redundant Architectures.

[BibT_eX]

[DOI]

Proceedings of the Applications in Electronics Pervading Industry, Environment and Society, 2021

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

Synthesis of P-Stable Abstractions.

[BibT_eX]

[DOI]

Anna Becchi

Enea Zaffanella

Proceedings of the Software Engineering and Formal Methods - 18th International Conference, 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

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

[BibT_eX]

[DOI]

Alessandro Abate

Muhammad Syifa'ul Mufid

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

Reactive Synthesis from Extended Bounded Response LTL Specifications.

[BibT_eX]

[DOI]

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

Temporal Planning with Intermediate Conditions and Effects.

[BibT_eX]

[DOI]

Alessandro Valentini

Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019

Formal reliability analysis of redundancy architectures.

[BibT_eX]

[DOI]

Cristian Mattarei

Formal Aspects Comput., 2019

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

[BibT_eX]

[DOI]

CoRR, 2019

COMPASS 3.0.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2019

NuRV: A nuXmv Extension for Runtime Verification.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 19th International Conference, 2019

Assumption-Based Runtime Verification with Partial Observability and Resets.

[BibT_eX]

[DOI]

Chun Tian

Proceedings of the Runtime Verification - 19th International Conference, 2019

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

[BibT_eX]

[DOI]

Muhammad Syifa'ul Mufid

Idriss Riouak

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

Robustness Envelopes for Temporal Plans.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019

2018

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

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2018

Tightening the contract refinements of a system architecture.

[BibT_eX]

[DOI]

Ramiro Demasi

Formal Methods Syst. Des., 2018

Strong temporal planning with uncontrollable durations.

[BibT_eX]

[DOI]

Artif. Intell., 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

Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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

Formal Specification and Verification of Dynamic Parametrized Architectures.

[BibT_eX]

[DOI]

Ivan Stojic

Proceedings of the Formal Methods - 22nd International Symposium, 2018

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

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

[BibT_eX]

[DOI]

Benjamin Bittner

Proceedings of the Model-Based Safety and Assessment - 5th International Symposium, 2017

SMT-based analysis of switching multi-domain linear Kirchhoff networks.

[BibT_eX]

[DOI]

Mirko Sessa

Proceedings of the 2017 Formal Methods in Computer Aided Design, 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

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017

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

Dynamic controllability via Timed Game Automata.

[BibT_eX]

[DOI]

Acta Informatica, 2016

The xSAP Safety Analysis Platform.

[BibT_eX]

[DOI]

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

Tightening a Contract Refinement.

[BibT_eX]

[DOI]

Ramiro Demasi

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

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

[BibT_eX]

[DOI]

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

Automated Synthesis of Timed Failure Propagation Graphs.

[BibT_eX]

[DOI]

Benjamin Bittner

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

From Electrical Switched Networks to Hybrid Automata.

[BibT_eX]

[DOI]

Mirko Sessa

Proceedings of the FM 2016: Formal Methods, 2016

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

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Verilog2SMV: A tool for word-level verification.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

Kristin Yvonne Rozier

Proceedings of the Computer Aided Verification - 28th International Conference, 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

A Lazy Approach to Temporal Epistemic Logic Model Checking.

[BibT_eX]

[DOI]

Marco Gario

Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies.

[BibT_eX]

[DOI]

Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

Automated Verification and Tightening of Failure Propagation Models.

[BibT_eX]

[DOI]

Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016

2015

Contracts-refinement proof system for component-based embedded systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

Safety assessment of AltaRica models via symbolic model checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

HRELTL: A temporal logic for hybrid systems.

[BibT_eX]

[DOI]

Inf. Comput., 2015

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

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Solving strong controllability of temporal problems with uncertainty using SMT.

[BibT_eX]

[DOI]

Constraints An Int. J., 2015

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

[BibT_eX]

[DOI]

Artif. Intell., 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

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

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2015

Comparing Different Functional Allocations in Automated Air Traffic Control Design.

[BibT_eX]

[DOI]

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

Formal Design and Safety Analysis of AIR6110 Wheel Brake System.

[BibT_eX]

[DOI]

Anthony Fernandes Pires

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

Efficient Anytime Techniques for Model-Based Safety Analysis.

[BibT_eX]

[DOI]

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

Formal Verification of Infinite-State BIP Models.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2015

Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

SMT-Based Validation of Timed Failure Propagation Graphs.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 2015

2014

Spacecraft early design validation using formal methods.

[BibT_eX]

[DOI]

Reliab. Eng. Syst. Saf., 2014

Quantifier-free encoding of invariants for hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Automated Planning and Model Checking (Dagstuhl Seminar 14482).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2014

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

[BibT_eX]

[DOI]

Proceedings of the 21st International Symposium on Temporal Representation and Reasoning, 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

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

[BibT_eX]

[DOI]

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

An Integrated Process for FDIR Design in Aerospace.

[BibT_eX]

[DOI]

Proceedings of the Model-Based Safety and Assessment - 4th International Symposium, 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

Formal Safety Assessment via Contract-Based Design.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013

Software Model Checking SystemC.

[BibT_eX]

[DOI]

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

SMT-based scenario verification for hybrid systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 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

OCRA: A tool for checking the refinement of temporal contracts.

[BibT_eX]

[DOI]

Michele Dorigatti

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Automated Analysis of Reliability Architectures.

[BibT_eX]

[DOI]

Cristian Mattarei

Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013

Efficient Analysis of Reliability Architectures via Predicate Abstraction.

[BibT_eX]

[DOI]

Cristian Mattarei

Proceedings of the Hardware and Software: Verification and Testing, 2013

Parameter synthesis with IC3.

[BibT_eX]

[DOI]

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

Time-aware relational abstractions for hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2013

SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

Timelines with Temporal Uncertainty.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, 2013

A Formal Framework for the Specification, Verification and Synthesis of Diagnosers.

[BibT_eX]

[DOI]

Proceedings of the Late-Breaking Developments in the Field of Artificial Intelligence, 2013

2012

Validation of requirements for hybrid systems: A formal approach.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2012

Software Model Checking with Explicit Scheduler and Symbolic Threads

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Verification of parametric system designs.

[BibT_eX]

[DOI]

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

A quantifier-free SMT encoding of non-linear hybrid automata.

[BibT_eX]

[DOI]

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

Application of SMT solvers to hybrid system verification.

[BibT_eX]

[DOI]

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

A Property-Based Proof System for Contract-Based Design.

[BibT_eX]

[DOI]

Proceedings of the 38th Euromicro Conference on Software Engineering and Advanced Applications, 2012

Solving Temporal Problems Using SMT: Strong Controllability.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2012

Software Model Checking via IC3.

[BibT_eX]

[DOI]

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

Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System.

[BibT_eX]

[DOI]

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

SMT-Based Verification of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

Solving Temporal Problems Using SMT: Weak Controllability.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

Symbolic Synthesis of Observability Requirements for Diagnosability.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence, 2012

2011

Formalizing requirements with object models and temporal constraints.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2011

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2011

Symbolic Model Checking and Safety Assessment of Altarica models.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Safety, Dependability and Performance Analysis of Extended AADL Models.

[BibT_eX]

[DOI]

Comput. J., 2011

Boosting Lazy Abstraction for SystemC with Partial Order Reduction.

[BibT_eX]

[DOI]

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

An Analytic Evaluation of SystemC Encodings in Promela.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2011

A Comprehensive Approach to On-Board Autonomy Verification and Validation.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2011, 2011

OthelloPlay: a plug-in based tool for requirement formalization and validation.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Developing Tools as Plug-ins, 2011

Proving and explaining the unfeasibility of message sequence charts for hybrid systems.

[BibT_eX]

[DOI]

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

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 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

From Sequential Extended Regular Expressions to NFA with Symbolic Labels.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 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

SMT-Based Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2010

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

[BibT_eX]

[DOI]

Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Model Checking of Hybrid Systems Using Shallow Synchronization.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2010

Applying SMT in symbolic execution of microcode.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Verifying SystemC: A software model checking approach.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

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

[BibT_eX]

[DOI]

Proceedings of 15th IEEE International Conference on Emerging Technologies and Factory Automation, 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

A Model Checker for AADL.

[BibT_eX]

[DOI]

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

RATSY - A New Requirements Analysis Tool with Synthesis.

[BibT_eX]

[DOI]

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

2009

Formalization and Validation of Safety-Critical Requirements

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2009

Verification and performance evaluation of aadl models.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2009

Model-Based Codesign of Critical Embedded Systems.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Supporting Requirements Validation: The EuRailCheck Tool.

[BibT_eX]

[DOI]

Proceedings of the ASE 2009, 2009

Structure-aware computation of predicate abstraction.

[BibT_eX]

[DOI]

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

Software model checking via large-block encoding.

[BibT_eX]

[DOI]

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

Requirements Validation for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Interpolant Generation for UTVPI.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Automated Planning.

[BibT_eX]

[DOI]

Marco Pistore

Proceedings of the Handbook of Knowledge Representation, 2008

Symbolic Compilation of PSL.

[BibT_eX]

[DOI]

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

Diagnostic Information for Realizability.

[BibT_eX]

[DOI]

Proceedings of the Verification, 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

Object Models with Temporal Constraints.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

Symbolic Computation of Schedulability Regions Using Parametric Timed Automata.

[BibT_eX]

[DOI]

Luigi Palopoli

Yusi Ramadian

Proceedings of the 29th IEEE Real-Time Systems Symposium, 2008

From Informal Requirements to Property-Driven Formal Validation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2008

The MathSAT 4SMT Solver.

[BibT_eX]

[DOI]

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

2007

Symbolic Implementation of Alternating Automata.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2007

Syntactic Optimizations for PSL Verification.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.

[BibT_eX]

[DOI]

Roberto Cavada

Krishnamani Kalyanasundaram

Anders Franzén

R. K. Shyamasundar

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Boolean Abstraction for Temporal Logic Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

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

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Verifying Heap-Manipulating Programs in an SMT Framework.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2007

Symbolic Fault Tree Analysis for Reactive Systems.

[BibT_eX]

[DOI]

Francesco Tapparo

Proceedings of the Automated Technology for Verification and Analysis, 2007

2006

Efficient theory combination via boolean search.

[BibT_eX]

[DOI]

Inf. Comput., 2006

Strong planning under partial observability.

[BibT_eX]

[DOI]

Artif. Intell., 2006

Symbolic Implementation of Alternating Automata.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2006

Building Efficient Decision Procedures on Top of SAT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Hardware Verification, 2006

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

[BibT_eX]

[DOI]

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 SMT(EUF ÈT).

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

From PSL to NBA: a Modular Symbolic Encoding.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Stong Cyclic Planning Under Partial Observability.

[BibT_eX]

Marco Pistore

Proceedings of the ECAI 2006, 17th European Conference on Artificial Intelligence, August 29, 2006

Formal analysis of hardware requirements.

[BibT_eX]

[DOI]

Proceedings of the 43rd Design Automation Conference, 2006

Towards Strong Cyclic Planning under Partial Observability.

[BibT_eX]

[DOI]

Marco Pistore

Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling, 2006

2005

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Encoding RTL Constructs for MathSAT: a Preliminary Report.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Preface.

[BibT_eX]

[DOI]

Alessandro Armando

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

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

[BibT_eX]

[DOI]

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

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The MathSAT 3 System.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

Verifying Industrial Hybrid Systems with MathSAT.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

Conformant planning via symbolic model checking and heuristic search.

[BibT_eX]

[DOI]

Artif. Intell., 2004

Bounded Verification of Past LTL.

[BibT_eX]

[DOI]

Daniel Sheridan

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems.

[BibT_eX]

Floris Roelofsen

Luciano Serafini

Proceedings of the 16th Eureopean Conference on Artificial Intelligence, 2004

Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains.

[BibT_eX]

Proceedings of the 16th Eureopean Conference on Artificial Intelligence, 2004

2003

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

[BibT_eX]

[DOI]

Artif. Intell., 2003

Bounded model checking.

[BibT_eX]

[DOI]

Adv. Comput., 2003

Bounded Model Checking for Past LTL.

[BibT_eX]

[DOI]

Marco Benedetti

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

Formal Verification of Diagnosability via Symbolic Model Checking.

[BibT_eX]

[DOI]

Charles Pecheur

Roberto Cavada

Proceedings of the IJCAI-03, 2003

A Framework for Planning with Extended Goals under Partial Observability.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth International Conference on Automated Planning and Scheduling (ICAPS 2003), 2003

2002

Improving the Encoding of LTL Model Checking into SAT.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2002

Integrating BDD-Based and SAT-Based Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

Bounded Model Checking for Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2002

Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking.

[BibT_eX]

Proceedings of the 15th European Conference on Artificial Intelligence, 2002

NuSMV 2: An OpenSource Tool for Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

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

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

Validation of Multiagent Systems by Symbolic Model Checking.

[BibT_eX]

[DOI]

Massimo Benerecetti

Proceedings of the Agent-Oriented Software Engineering III, Third International Workshop, 2002

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

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence, 2002

Improving Heuristics for Planning as Search in Belief Space.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Conference on Artificial Intelligence Planning Systems, 2002

2001

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

[BibT_eX]

[DOI]

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.

[BibT_eX]

Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning.

[BibT_eX]

Vicky Hartonas-Garmhausen

Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

2000

NUSMV: A New Symbolic Model Checker.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2000

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

[BibT_eX]

[DOI]

Sérgio Vale Aguiar Campos

Edmund M. Clarke

Fausto Giunchiglia

Sci. Comput. Program., 2000

Conformant Planning via Symbolic Model Checking.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2000

Industrial Applications of Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

1999

Preface.

[BibT_eX]

[DOI]

Orna Grumberg

Proceedings of the First International Workshop on Symbolic Model Checking, 1999

Symbolic Model Checking without BDDs.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1999

Formal Specification and Validation of a Vital Communication Protocol.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

Conformant Planning via Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Recent Advances in AI Planning, 5th European Conference on Planning, 1999

Symbolic Model Checking Using SAT Procedures instead of BDDs.

[BibT_eX]

[DOI]

Proceedings of the 36th Conference on Design Automation, 1999

NUSMV: A New Symbolic Model Verifier.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Formal Verification of a Railway Interlocking System using Model Checking.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1998

A Many-Sorted Natural Deduction.

[BibT_eX]

[DOI]

Fausto Giunchiglia

Richard W. Weyhrauch

Comput. Intell., 1998

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

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1998

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

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1998

Strong Planning in Non-Deterministic Domains Via Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, 1998

Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains.

[BibT_eX]

[DOI]