Marco Roveri

According to our database1, Marco Roveri
  • authored at least 86 papers between 1996 and 2017.
  • has a "Dijkstra number"2 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

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

Satisfiability Modulo Transcendental Functions via Incremental Linearization.
Proceedings of the Automated Deduction - CADE 26, 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
Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2016

Dynamic controllability via Timed Game Automata.
Acta Inf., 2016

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

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

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

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

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

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty.
Artif. Intell., 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

2014
Spacecraft early design validation using formal methods.
Rel. Eng. & Sys. Safety, 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

The nuXmv Symbolic Model Checker.
Proceedings of the Computer Aided Verification - 26th International Conference, 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

Preface to the special section on Formal Methods for Industrial Critical Systems (FMICS 2009 + FMICS 2010).
Sci. Comput. Program., 2013

Timelines with Temporal Uncertainty.
Proceedings of the Twenty-Seventh AAAI Conference on 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
Logical Methods in Computer Science, 2012

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

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

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

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

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

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

Conformant Planning via Symbolic Model Checking
CoRR, 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

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

2010
From Sequential Extended Regular Expressions to NFA with Symbolic Labels.
Proceedings of the Implementation and Application of Automata, 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

Semi-formal functional verification by EFSM traversing via NuSMV.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2010

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

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

A Model Checker for AADL.
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

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

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

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

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

Diagnostic Information for Realizability.
Proceedings of the Verification, 2008

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

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

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

Preface.
Electr. Notes Theor. Comput. Sci., 2007

Syntactic Optimizations for PSL Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

RAT: A Tool for the Formal Analysis of Requirements.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

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

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

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

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

2004
Specifying and analyzing early requirements in Tropos.
Requir. Eng., 2004

Requirements-Driven Verification of Web Services.
Electr. Notes Theor. Comput. Sci., 2004

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

Formal Verification of Requirements using SPIN: A Case Study on Web Services.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

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

A Framework for Integrating Business Processes and Business Requirements.
Proceedings of the 8th International Enterprise Distributed Object Computing Conference (EDOC 2004), 2004

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

Specifying and Analyzing Early Requirements: Some Experimental Results.
Proceedings of the 11th IEEE International Conference on Requirements Engineering (RE 2003), 2003

Agent-Oriented Modeling by Interleaving Formal and Informal Specification.
Proceedings of the Agent-Oriented Software Engineering IV, 4th International Workshop, 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

NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 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.
STTT, 2000

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

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

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

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
A New Method for Testing Decision Procedures in Modal Logics.
Proceedings of the Automated Deduction, 1997

1996
A New Method for Testing Decision Procedures in Modal and Terminological Logics.
Proceedings of the 1996 International Workshop on Description Logics, 1996


  Loading...