Alessandro Cimatti - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

A Comprehensive Approach to On-Board Autonomy Verification and ValidationMarco Bozzano, Alessandro Cimatti, Marco Roveri, Andrei Tchaltsev. IJCAI 2011: 2398-2403 [doi]

Safety, Dependability and Performance Analysis of Extended AADL ModelsMarco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. cj, 54(5):754-775, 2011. [doi]

An Analytic Evaluation of SystemC Encodings in PromelaDaniele Campana, Alessandro Cimatti, Iman Narasamdya, Marco Roveri. spin 2011: 90-107 [doi]

Computing Small Unsatisfiable Cores in Satisfiability Modulo TheoriesAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. jair, 40:701-728, 2011. [doi]

Efficient Scenario Verification for Hybrid AutomataAlessandro Cimatti, Sergio Mover, Stefano Tonetta. cav 2011: 317-332 [doi]

Boosting Lazy Abstraction for SystemC with Partial Order ReductionAlessandro Cimatti, Iman Narasamdya, Marco Roveri. TACAS 2011: 341-356 [doi]

Kratos - A Software Model Checker for SystemCAlessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri. cav 2011: 310-316 [doi]

Formalizing requirements with object models and temporal constraintsAlessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta. SoSyM, 10(2):147-160, 2011. [doi]

2010

RATSY - A New Requirements Analysis Tool with SynthesisRoderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber. cav 2010: 425-429 [doi]

A Model Checker for AADLMarco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. cav 2010: 562-565 [doi]

Model Checking of Hybrid Systems Using Shallow SynchronizationLei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta. forte 2010: 155-169 [doi]

Formalization and validation of a subset of the European Train Control SystemAngelo Chiappini, Alessandro Cimatti, Luca Macchi, Oscar Rebollo, Marco Roveri, Angelo Susi, Stefano Tonetta, Berardino Vittorini. ICSE 2010: 109-118 [doi]

Satisfiability Modulo the Theory of Costs: Foundations and ApplicationsAlessandro Cimatti, Anders FranzÃ©n, Alberto Griggio, Roberto Sebastiani, Cristian Stenico. TACAS 2010: 99-113 [doi]

From Sequential Extended Regular Expressions to NFA with Symbolic LabelsAlessandro Cimatti, Sergio Mover, Marco Roveri, Stefano Tonetta. wia 2011: 87-94 [doi]

Efficient generation of craig interpolants in satisfiability modulo theoriesAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. tocl, 12(1):7, 2010. [doi]

Tighter integration of BDDs and SMT for Predicate AbstractionAlessandro Cimatti, Anders Franzén, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri. date 2010: 1707-1712 [doi]

Verifying SystemC: A software model checking approachAlessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri. FMCAD 2010: 51-59 [doi]

SMT-Based Software Model CheckingAlessandro Cimatti. spin 2010: 1-3 [doi]

Applying SMT in symbolic execution of microcodeAnders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev. FMCAD 2010: 121-128 [doi]

2009

Software model checking via large-block encodingDirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani. FMCAD 2009: 25-32 [doi]

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace SystemsMarco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. safecomp 2009: 173-186 [doi]

Codesign of dependable systems: A component-based modeling languageMarco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. memocode 2009: 121-130 [doi]

Verification and performance evaluation of aadl modelsMarco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. FSE 2009: 285-286 [doi]

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysisRoberto Bruttomesso, Alessandro Cimatti, Anders FranzÃ©n, Alberto Griggio, Roberto Sebastiani. AMAI, 55(1-2):63-99, 2009. [doi]

Supporting Requirements Validation: The EuRailCheck ToolRoberto Cavada, Alessandro Cimatti, Alessandro Mariotti, Cristian Mattarei, Andrea Micheli, Sergio Mover, Marco Pensallorto, Marco Roveri, Angelo Susi, Stefano Tonetta. kbse 2009: 665-667 [doi]

Requirements Validation for Hybrid SystemsAlessandro Cimatti, Marco Roveri, Stefano Tonetta. cav 2009: 188-203 [doi]

Interpolant Generation for UTVPIAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. cade 2009: 167-182 [doi]

Structure-aware computation of predicate abstractionAlessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri. FMCAD 2009: 9-16 [doi]

2008

The MathSAT 4SMT SolverRoberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. cav 2008: 299-303 [doi]

Efficient Interpolant Generation in Satisfiability Modulo TheoriesAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. TACAS 2008: 397-412 [doi]

Symbolic Compilation of PSLAlessandro Cimatti, Marco Roveri, Stefano Tonetta. tcad, 27(10):1737-1750, 2008. [doi]

Symbolic Computation of Schedulability Regions Using Parametric Timed AutomataAlessandro Cimatti, Luigi Palopoli, Yusi Ramadian. rtss 2008: 80-89 [doi]

From Informal Requirements to Property-Driven Formal ValidationAlessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta. fmics 2009: 166-181 [doi]

Diagnostic Information for RealizabilityAlessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev. vmcai 2008: 52-67 [doi]

Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008Alessandro Cimatti, Robert B. Jones, editors, IEEE, 2008.

Object Models with Temporal ConstraintsAlessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta. sefm 2008: 249-258 [doi]

2007

Symbolic Implementation of Alternating AutomataRoderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri. ijfcs, 18(4):727-743, 2007. [doi]

Symbolic Fault Tree Analysis for Reactive SystemsMarco Bozzano, Alessandro Cimatti, Francesco Tapparo. ATVA 2007: 162-176 [doi]

A Lazy and Layered SMT( /mathcal{BV} ) Solver for Hard Industrial Verification ProblemsRoberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani. cav 2007: 547-560 [doi]

Computing Predicate Abstractions by Integrating BDDs and SMT SolversRoberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar. FMCAD 2007: 69-76 [doi]

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo TheoriesAlessandro Cimatti, Alberto Griggio, Roberto Sebastiani. sat 2007: 334-339 [doi]

Boolean Abstraction for Temporal Logic SatisfiabilityAlessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta. cav 2007: 532-546 [doi]

Syntactic Optimizations for PSL VerificationAlessandro Cimatti, Marco Roveri, Stefano Tonetta. TACAS 2007: 505-518 [doi]

Verifying Heap-Manipulating Programs in an SMT FrameworkZvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. ATVA 2007: 237-252 [doi]

2006

PrefaceAlessandro Armando, Alessandro Cimatti. ENTCS, 144(2):1-2, 2006. [doi]

Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced LecturesMarco Bernardo, Alessandro Cimatti, editors, Volume 3965 of Lecture Notes in Computer Science, Springer, 2006.

Strong planning under partial observabilityPiergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso. ai, 170(4-5):337-384, 2006. [doi]

Towards Strong Cyclic Planning under Partial ObservabilityPiergiorgio Bertoli, Alessandro Cimatti, Marco Pistore. aips 2006: 354-357

Stong Cyclic Planning Under Partial ObservabilityPiergiorgio Bertoli, Alessandro Cimatti, Marco Pistore. ecai 2006: 580-584

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and SynthesisPiergiorgio Bertoli, Marco Bozzano, Alessandro Cimatti. mochart 2007: 1-18 [doi]

Symbolic Implementation of Alternating AutomataRoderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri, Simone Semprini. wia 2006: 208-218 [doi]

Encoding RTL Constructs for MathSAT: a Preliminary ReportMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani. ENTCS, 144(2):3-14, 2006. [doi]

Efficient theory combination via boolean searchMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani. iandc, 204(10):1493-1525, 2006. [doi]

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in ::::SMT::::(::::EUF:::: È::::T::::)Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani. lpar 2006: 557-571 [doi]

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative AnalysisRoberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. lpar 2006: 527-541 [doi]

From PSL to NBA: a Modular Symbolic EncodingAlessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta. FMCAD 2006: 125-133 [doi]

Building Efficient Decision Procedures on Top of SAT SolversAlessandro Cimatti, Roberto Sebastiani. sfm 2006: 144-175 [doi]

Formal analysis of hardware requirementsIngo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem, Alessandro Cimatti. dac 2006: 821-826 [doi]

2005

Verifying Industrial Hybrid Systems with MathSATGilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani. ENTCS, 119(2):17-32, 2005. [doi]

Efficient Satisfiability Modulo Theories via Delayed Theory CombinationMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani. cav 2005: 335-349 [doi]

MathSAT: Tight Integration of SAT and Mathematical Decision ProceduresMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. JAR, 35(1-3):265-293, 2005. [doi]

The MathSAT 3 SystemMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. cade 2005: 315-321 [doi]

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic LogicMarco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. TACAS 2005: 317-333 [doi]

2004

2003

2002

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and RequirementsGilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. AISC 2002: 231-245 [doi]

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical PropositionsGilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. cade 2002: 195-210 [doi]

Bounded Model Checking for Timed SystemsGilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. forte 2002: 243-259 [doi]

Validation of Multiagent Systems by Symbolic Model CheckingMassimo Benerecetti, Alessandro Cimatti. aose 2003: 32-46 [doi]

Improving Heuristics for Planning as Search in Belief SpacePiergiorgio Bertoli, Alessandro Cimatti. aips 2002: 143-152

Solving Power Supply Restoration Problems with Planning via Symbolic Model CheckingPiergiorgio Bertoli, Alessandro Cimatti, John K. Slaney, Sylvie Thiébaux. ecai 2002: 576-580

Integrating BDD-Based and SAT-Based Symbolic Model CheckingAlessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella. frocos 2002: 49-56 [doi]

Improving the Encoding of LTL Model Checking into SATAlessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani. vmcai 2002: 196-207 [doi]

NuSMV 2: An OpenSource Tool for Symbolic Model CheckingAlessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella. cav 2002: 359-364 [doi]

2001

Planning in Nondeterministic Domains under Partial Observability via Symbolic Model CheckingPiergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso. IJCAI 2001: 473-478

Heuristic Search + Symbolic Model Checking = Efficient Conformant PlanningPiergiorgio Bertoli, Alessandro Cimatti, Marco Roveri. IJCAI 2001: 467-472

Searching Powerset Automata by Combining Explicit-State and Symbolic Model CheckingAlessandro Cimatti, Marco Roveri, Piergiorgio Bertoli. TACAS 2001: 313-327 [doi]

2000

1999

Symbolic Model Checking without BDDsArmin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu. TACAS 1999: 193-207 [doi]

Symbolic Model Checking Using SAT Procedures instead of BDDsArmin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu. dac 1999: 317-320 [doi]

Formal Specification and Development of a Safety-Critical Train Management SystemA. Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita. safecomp 1999: 410-419 [doi]

PrefaceAlessandro Cimatti, Orna Grumberg. ENTCS, 23(2), 1999. [doi]

Formal Specification and Validation of a Vital Communication ProtocolAlessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita. fm 1999: 1584-1604 [doi]

Conformant Planning via Model CheckingAlessandro Cimatti, Marco Roveri. ecp 2000: 21-34

NUSMV: A New Symbolic Model VerifierAlessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri. cav 1999: 495-499 [doi]

1998

A Structured Approach to the Formal Certification of Safety of Computer Aided Development ToolsPiergiorgio Bertoli, Alessandro Cimatti, Fausto Giunchiglia, Paolo Traverso. safecomp 1998: 221-230 [doi]

A Many-Sorted Natural DeductionAlessandro Cimatti, Fausto Giunchiglia, Richard W. Weyhrauch. ci, 14:134-149, 1998.

Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic DomainsAlessandro Cimatti, Marco Roveri, Paolo Traverso. AAAI 1998: 875-881

Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking SystemAlessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso. safecomp 1998: 284-295 [doi]

Verification of a Safety-Critical Railway Interlocking System with Real-Time ConstraintsVicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia. ftcs 1998: 458-463

PreviousNext