Alessandro Cimatti

Publications

1. Bombardelli Alberto; Bonizzi Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nicolodi Edoardo; Tonetta Stefano; Zampedri Gianni, COMPASTA = COMPASS + TASTE
2. Becchi Anna; Cimatti Alessandro; Zaffanella Enea, P-stable abstractions of hybrid systems
3. Tosello Elisa; Bonel Paolo; Buranello Alberto; Carraro Marco; Cimatti Alessandro; Granelli Lorenzo; Panjkovic Stefan; Micheli Andrea, Opportunistic (Re)planning for Long-Term Deep-Ocean Inspection: An Autonomous Underwater Architecture
4. Bombardelli Alberto; Cimatti Alessandro; Tonetta Stefano; Zamboni Marco, Symbolic Model Checking of Relative Safety LTL Properties
5. Koenig Lukas; Heinzemann Christian; Griggio Alberto; Klauck Michaela; Cimatti Alessandro; Henze Franziska; Tonetta Stefano; Kueperkoch Stefan; Fassbender Dennis; Hanselmann Michael, Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development
6. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto; Mcmillan Kenneth, Invariant Checking for SMT-based Systems with Quantifiers
7. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
8. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano; Bonafini Federico; Campidelli Matteo; Zasa Andrea, Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report
9. Xia Yechuan; Cimatti Alessandro; Griggio Alberto; Li Jianwen, Avoiding the Shoals - A New Approach to Liveness Checking
10. Basagiannis Stylianos; Battista Ludovico; Becchi Anna; Cimatti Alessandro; Giantamidis Georgios; Mover Sergio; Tacchella Alberto; Tonetta Stefano; Tsachouridis Vassilios, Stability Verification of an Industrial Switched PI Control Systems
11. Becchi Anna; Cimatti Alessandro; Scaglione Giuseppe, Testing the Migration from Analog to Software-Based Railway Interlocking Systems
12. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto, Towards Verification Modulo Theories of asynchronous systems via abstraction refinement
13. Becchi Anna; Cimatti Alessandro, Abstraction Modulo Stability
14. Cappelletti Lorenzo; Cavada Roberto; Cimatti Alessandro; Keppel Marco, Towards the Formal Analysis of Algorithmic Requirements
15. Bozzano Marco; Cimatti Alessandro; Cristoforetti Marco; Griggio Alberto; Svaizer Piergiorgio; Tonetta Stefano, Towards Formal Design of FDIR Components with AI
16. Diedrich Alexander; Heesch René; Bozzano Marco; Ludwig Björn; Cimatti Alessandro; Niggemann Oliver, Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory
17. Bombardelli Alberto; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano, Another Look at LTL Modulo Theory over Finite and Infinite Traces
18. Sharifzadeh Mojtaba; Beirami Hani; Bonafini Federico; Campidelli Matteo; Cavada Roberto; Cimatti Alessandro; Tonetta Stefano, A Switching Event-Triggered Model Predictive Control for HVAC Systems
19. Cimatti Alessandro; Khandaker Shaker; Kifetew Fitsum; Leone Lorenzo; Prandi Davide; Scaglione Giuseppe; Susi Angelo; Turboli Orazio, Model-Based Testing of Railway Interlocking Systems
20. Cimatti Alessandro; Moller Grosen Thomas; Larsen Kim G.; Tonetta Stefano; Zimmermann Martin, Exploiting Assumptions for Effective Monitoring of Real-Time Properties Under Partial Observability
21. Sumic Ajdin; Cimatti Alessandro; Micheli Andrea; Vidal Thierry, SMT-Based Repair of Disjunctive Temporal Networks with Uncertainty: Strong and Weak Controllability
22. Sumic Ajdin; Vidal Thierry; Micheli Andrea; Cimatti Alessandro, Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning
23. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, GR(1) is equivalent to R(1)
24. Cimatti Alessandro; Cristoforetti Luca; Griggio Alberto; Tonetta Stefano; Corfini Sara; Di Natale Marco; Barrau Florian, EVA: a Tool for the Compositional Verification of AUTOSAR Models
25. Xia Yechuan; Becchi Anna; Cimatti Alessandro; Griggio Alberto; Li Jianwen; Pu Geguang, Searching for i-Good Lemmas to Accelerate Safety Model Checking
26. Tierno Antonio; Turri Giuliano; Cimatti Alessandro; Passerone Roberto, Scalable Design Space Exploration for the Synthesis of Redundant Architectures
27. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Susi Angelo, A Formal IDE for Railways: Research Challenges
28. Basagiannis Stylianos; Battista Ludovico; Becchi Anna; Cimatti Alessandro; Giantamidis Georgios; Mover Sergio; Tacchella Alberto; Tonetta Stefano; Tsachouridis Vassilios, SMT-Based Stability Verification of an Industrial Switched PI Control Systems
29. Lanzani Isabella; Scattolini Riccardo; Zio Enrico; Cimatti Alessandro; Bozzano Marco; Tonetta Stefano, Two formal methodologies of Model-Based Safety Assessment for Fault Tree Analysis
30. Bombardelli Alberto; Bonizzi Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nazaria Massimo; Nicolodi Edoardo; Tonetta Stefano; Zampedri Gianni, COMPASTA: Integrating COMPASS Functionality into TASTE
31. Casagrande Alberto; Cimatti Alessandro; Dorigo Luca; Piazza Carla; Tonetta Stefano, Set-Based Invariants over Polynomial Systems
32. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, A first-order logic characterization of safety and co-safety languages
33. Stefenon Stefano Frizzo; Cristoforetti Marco; Cimatti Alessandro, Towards Automatic Digitalization of Railway Engineering Schematics
34. Bozzano Marco; Cimatti Alessandro; Tonetta Stefano; Vozárová Viktória, Searching for Ribbon-Shaped Paths in Fair Transition Systems
35. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Jonas Martin, Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
36. Panjkovic Stefan; Micheli Andrea; Cimatti Alessandro, Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping
37. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano; Vozárová Viktória, Diagnosability of fair transition systems
38. Tierno A.; Turri G.; Cimatti A.; Passerone R., Automatic Design Space Exploration of Redundant Architectures
39. Stefenon Stefano Frizzo; Singh Gurmail; Yow Kin-Choong; Cimatti Alessandro, Semi-ProtoPNet Deep Neural Network for the Classification of Defective Power Grid Distribution Structures
40. Cimatti A.; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, A first-order logic characterisation of safety and co-safety languages
41. Amendola Arturo; Becchi Anna; Cavada Roberto; Cimatti Alessandro; Ferrando Andrea; Pilati Lorenzo; Scaglione Giuseppe; Tacchella Alberto; Zamboni Marco, NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
42. Becchi Anna; Cimatti Alessandro, Abstraction Modulo Stability for Reverse Engineering
43. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Jonas Martin; Kimberly Greg, Analysis of Cyclic Fault Propagation via ASP
44. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, LTL falsification in infinite-state systems
45. Bombardelli Alberto; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Nazaria Massimo; Nicolodi Edoardo; Tonetta Stefano, COMPASTA: Extending TASTE with Formal Design and Verification Functionality
46. Amendola Arturo; Barruffo Lorenzo; Bozzano Marco; Cimatti Alessandro; De Simone Salvatore; Fedeli Eugenio; Gabbasov Artem; Ernesto Garrubba Domenico; Girardi Massimiliano; Serra Diana; Tiella Roberto; Zampedri Gianni, Formal Design and Validation of an Automatic Train Operation Control System
47. Cimatti Alessandro; Corfini Sara; Cristoforetti Luca; Di Natale Marco; Griggio Alberto; Puri Stefano; Tonetta Stefano, A comprehensive framework for the analysis of automotive systems
48. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Verification of SMT Systems with Quantifiers
49. Cimatti Alessandro; Griggio Alberto; Lipparini Enrico; Sebastiani Roberto, Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test
50. Cimatti Alessandro; Griggio Alberto; Tonetta Stefano, The VMT-LIB Language and Tools
51. Cimatti Alessandro; Tian Chun; Tonetta Stefano, Assumption-based Runtime Verification
52. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Jones David; Mattarei Cristian, Model-based Safety Assessment of a Triple Modular Generator with XSAP
53. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning
54. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, Proving the Existence of Fair Paths in Infinite-State Systems
55. Bozzano Marco; Cimatti Alessandro; Fernandes Pires Anthony; Griggio Alberto; Jonas Martin; Kimberly Greg, Efficient SMT-Based Analysis of Failure Propagation
56. Bozzano Marco; Cimatti Alessandro; Roveri Marco, A Comprehensive Approach to On-board Autonomy Verification and Validation
57. Cimatti Alessandro; Tian Chun; Tonetta Stefano, Assumption-Based Runtime Verification of Infinite-State Systems
58. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
59. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, Expressiveness of Extended Bounded Response LTL
60. Syifa'ul Mufid Muhammad; Micheli Andrea; Abate Alessandro; Cimatti Alessandro, SMT-Based Model Checking of Max-Plus Linear Systems
61. Cashmore Michael; Cimatti Alessandro; Magazzeni Daniele; Micheli Andrea; Zehtabi Parisa, Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans
62. Mover Sergio; Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Tonetta Stefano, Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
63. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis
64. Bartali Ruben; Christodoulaki Rosie; Drosou Vassiliki; Baker Derek Keith; Svaizer Piergiorgio; Alarcón-Padilla Diego-César; Osório Tiago; Kramer Wolfgang; Bolognese Michele; Pratticò Luca; Viesi Diego; Roca Sobrino Lidia; Guillen Burrieza Elena; Fluch Juergen; Bayer Özgür; Pınarlı Deniz; Erdoğan Selin; Brunner Christoph; Cavada Roberto; Bonizzi Alberto; Cimatti Alessandro; Zanetti Alberto; Crema Luigi, Decarbonization of industrial processes: technologies, applications and perspectives of low-temperature solar heat (80-150°C)
65. Becchi Anna; Cimatti Alessandro; Zaffanella Enea, Reverse engineering with P-stable Abstractions
66. Bigarella Filippo; Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Jonáš Martin; Roveri Marco; Sebastiani Roberto; Trentin Patrick, Optimization Modulo Non-linear Arithmetic via Incremental Linearization
67. Cimatti Alessandro; Griggio Alberto; Magnago Enrico, Automatic Discovery of Fair Paths in Infinite-State Transition Systems
68. Cimatti Alessandro; Griggio Alberto; Magnago Enrico; Roveri Marco; Tonetta Stefano, SMT-Based Satisfiability of First-Order LTL with Event Freezing Functions and Metric Operators
69. Valentini Alessandro; Micheli Andrea; Cimatti Alessandro, Temporal Planning with Intermediate Conditions and Effects
70. Cimatti Alessandro; Geatti Luca; Gigante Nicola; Montanari Angelo; Tonetta Stefano, Reactive Synthesis from Extended Bounded Response LTL Specifications
71. Cimatti Alessandro; Geatti Luca; Griggio Alberto; Kimberly Greg; Tonetta Stefano, Safe Decomposition of Startup Requirements: Verification and Synthesis
72. Abate Alessandro; Cimatti Alessandro; Micheli Andrea; Mufid Muhammad Syifa’ul, Computation of the Transient in Max-Plus Linear Systems via SMT-Solving
73. Beirami H.; Calzà D.; Cimatti A.; Islam M. M.; Roveri M.; Svaizer P., Predicting RUL of Bearings in the Pumps of a Critical Industrial Air Treatment System
74. Beirami H.; Calzà D.; Cimatti A.; Islam M.; Roveri M.; Svaizer P., A Data-driven Approach for RUL Prediction of an Experimental Filtration System
75. Amendola Arturo; Becchi Anna; Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Scaglione Giuseppe; Susi Angelo; Tacchella Alberto; Tessi Matteo, A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System
76. Becchi Anna; Cimatti Alessandro; Zaffanella Enea, Synthesis of P-Stable Abstractions
77. Bozzano M.; Cimatti A.; Mattarei C., Formal reliability analysis of redundant architectures
78. Bozzano Marco; Bruintjes Harold; Cimatti Alessandro; Katoen Joost-Pieter; Noll Thomas; Tonetta Stefano, COMPASS 3.0
79. Cashmore Michael; Cimatti Alessandro; Magazzeni Daniele; Micheli Andrea; Zehtabi Parisa, Robustness Envelopes for Temporal Plans
80. Cimatti Alessandro; Griggio Alberto; Magnago Enrico; Roveri Marco; Tonetta Stefano, Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
81. Cimatti Alessandro; Delong Rance; Stojic Ivan; Tonetta Stefano, Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems
82. Cimatti Alessandro; Tian Chun; Tonetta Stefano, Assumption-based Runtime Verification with Partial Observability and Resets
83. Cimatti Alessandro; Tian Chun; Tonetta Stefano, NuRV: a nuXmv Extension for Runtime Verification
84. Cimatti Alessandro; Do Minh; Micheli Andrea; Roveri Marco; Smith David E., Strong temporal planning with uncontrollable durations
85. Cimatti Alessandro; Demasi Ramiro Adrian; Tonetta Stefano, Tightening the contract refinements of a system architecture
86. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
87. Cimatti Alessandro; Stojic Ivan; Tonetta Stefano, Formal Specification and Verification of Dynamic Parametrized Architectures
88. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
89. Cavada Roberto; Cimatti Alessandro; Mover Sergio; Sessa Mirko; Cadavero Giuseppe; Scaglione Giuseppe, Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
90. Cimatti Alessandro; Ghilardi Silvio; Ranise Silvio, Model checking: teoria ed applicazioni
91. Mechtaev Sergey; Griggio Alberto; Cimatti Alessandro; Roychoudhury Abhik, Symbolic execution with existential second-order constraints
92. Cimatti Alessandro; Delong Rance; Stojic Ivan; Tonetta Stefano, Towards Adaptive MILS Systems: Model-Based Design, Verification And Run-Time Adaptation
93. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
94. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
95. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Satisfiability Modulo Transcendental Functions via Incremental Linearization
96. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic
97. Cimatti Alessandro; Mover Sergio; Sessa Mirko, SMT-based analysis of switching multi-domain linear Kirchhoff networks
98. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro, Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study
99. Bozzano Marco; Bruintjes Harold; Cimatti Alessandro; Katoen Joost-Pieter; Noll Thomas; Tonetta Stefano, Formal Methods for Aerospace Systems
100. Bittner Benjamin; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Gario Marco Elio Gustavo; Griggio Alberto; Mattarei Cristian; Micheli Andrea; Zampedri Gianni, The xSAP Safety Analysis Platform
101. Cimatti Alessandro; Hunsberger Luke; Micheli Andrea; Posenato Roberto; Roveri Marco, Dynamic controllability via Timed Game Automata
102. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Zampedri Gianni, Automated Verification and Tightening of Failure Propagation Models
103. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro, Automated Synthesis of Timed Failure Propagation Graphs
104. Ábrahám Erika; Abbott John; Becker Bernd; Bigatti Anna M.; Brain Martin; Buchberger Bruno; Cimatti Alessandro; Davenport James H.; England Matthew; Fontaine Pascal; Forrest Stephen; Griggio Alberto; Kroening Daniel; Seiler Werner M.; Sturm Thomas, SC^2: Satisfiability Checking Meets Symbolic Computation
105. Jakub Daniel; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano; Mover Sergio, Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
106. Irfan Ahmed; Cimatti Alessandro; Griggio Alberto; Roveri Marco; Sebastiani Roberto, Verilog2SMV: A Tool for Word-level Verification
107. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies
108. Gario Marco Elio Gustavo; Cimatti Alessandro; Mattarei Cristian; Tonetta Stefano; Rozier Kristin Yvonne, Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
109. Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, A Lazy Approach to Temporal Epistemic Logic Model Checking
110. Cimatti Alessandro; Demasi Ramiro Adrian; Tonetta Stefano, Tightening a Contract Refinement
111. Cimatti Alessandro; Mover S.; Sessa Mirko, From Electrical Switched Networks to Hybrid Automata
112. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Infinite-state invariant checking with IC3 and predicate abstraction
113. Cavada Roberto; Cimatti Alessandro; Crema Luigi; Roccabruna Mattia; Tonetta Stefano, Model-Based Design of an Energy-System Embedded Controller Using Taste
114. Ábrahám E.; Fontaine P.; Forrest S.; Griggio A.; Kroening D.; Seiler W. M.; Sturm T.; Abbott J.; Becker B.; Bigatti A. M.; Brain M.; Buchberger B.; Cimatti A.; Davenport J. H.; England M., Satisfiability checking and symbolic computation
115. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Solving strong controllability of temporal problems with uncertainty using SMT
116. Cimatti Alessandro; Tonetta Stefano, Contracts-refinement proof system for component-based embedded systems
117. Bozzano Marco; Cimatti Alessandro; Oleg Lisagor; Mattarei Cristian; Mover Sergio; Roveri Marco; Tonetta Stefano, Safety Assessment of AltaRica Models via Symbolic Model Checking
118. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach
119. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Micheli Andrea, SMT-based Validation of Timed Failure Propagation Graphs
120. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, HYCOMP - an SMT-based model checker for hybrid systems
121. Cimatti Alessandro; Micheli Andrea; Roveri Marco, An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
122. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
123. Cimatti Alessandro; Roveri Marco; Tonetta Stefano, HRELTL: A temporal logic for hybrid systems
124. Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Mattarei Cristian, Efficient Anytime Techniques for Model-Based Safety Analysis
125. Mattarei Cristian; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano; Rozier Kristin Yvonne, Comparing Different Functional Allocations in Automated Air Traffic Control Design
126. Bliudze Simon; Cimatti Alessandro; Jaber Mohamad; Mover Sergio; Roveri Marco; Saab Wajeb; Wang Qiang, Formal Verification of Infinite-State BIP Models
127. Bozzano Marco; Cimatti Alessandro; Fernandes Pires Anthony; Jones D.; Kimberly G.; Petri T.; Robinson R.; Tonetta Stefano, Formal Design and Safety Analysis of AIR6110 Wheel Brake System
128. Cimatti Alessandro; Delong Rance; Marcantonio Davide; Tonetta Stefano, Combining MILS with Contract-Based Design for Safety and Security Requirements
129. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic
130. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, Quantifier-free encoding of invariants for hybrid systems
131. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, IC3 Modulo Theories via Implicit Predicate Abstraction
132. Robin Steel; Alexander Hoffmann; Marc Niezette; Cimatti Alessandro; Roveri Marco; Konstantinos Kapellos; Alessandro Donati; Nicola Policella, Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Concluding the adventure
133. Bozzano Marco; Cimatti Alessandro; Katoen J. P.; Katsaros P.; Mokos K.; Nguyen V. Y.; Noll T.; Postma B.; Roveri Marco, Spacecraft Early Design Validation using Formal Methods
134. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Verifying LTL Properties of Hybrid Systems with K-Liveness
135. Cavada Roberto; Cimatti Alessandro; Dorigatti Michele; Griggio Alberto; Mariotti Alessandro; Micheli Andrea; Mover Sergio; Roveri Marco; Tonetta Stefano, The nuXmv Symbolic Model Checker
136. Bozzano Marco; Cimatti Alessandro; Mattarei Cristian; Tonetta Stefano, Formal Safety Assessment via Contract-Based Design.
137. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Griggio Alberto, Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions
138. Cimatti Alessandro; Hunsberger L.; Micheli Andrea; Roveri Marco, Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty
139. Cimatti Alessandro; Hunsberger L.; Micheli Andrea; Posenato R; Roveri Marco, Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation
140. Guiotto A.; De Ferluc R.; Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Yushtein Y., FAME Process: A Dedicated Development and V&V Process for FDIR
141. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; De Ferluc R.; Gario Marco Elio Gustavo; Guiotto A.; Yushtein Y., An Integrated Process for FDIR Design in Aerospace
142. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; De Ferluc R.; Gario Marco Elio Gustavo; Guiotto A.; Yushtein Y., FAME: A Model-Based Environment for FDIR Design in Aerospace
143. Laura Baracchi; Cimatti Alessandro; Gerald Garcia; Silvia Mazzini; Stefano Puri; Tonetta Stefano, Requirements Refinement and Component Reuse: The FoReVer Contract-Based Approach
144. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, SMT-based scenario verification for hybrid systems
145. Bozzano Marco; Cimatti Alessandro; Mattarei Cristian, Automated Analysis of Reliability Architectures
146. Cimatti Alessandro; Narasamdya Iman; Roveri Marco, Software Model Checking SystemC
147. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Timelines with Temporal Uncertainty
148. Cimatti Alessandro; Griggio Alberto; Bastiaan Joost Schaafsma; Roberto Sebastiani, The MathSAT5 SMT Solver
149. Cimatti Alessandro; Griggio Alberto; Bastiaan Joost Schaafsma; Roberto Sebastiani, A Modular Approach to MaxSAT Modulo Theories
150. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, A Formal Framework for the Specification, Verification and Synthesis of Diagnosers
151. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, Formal Specification and Synthesis of FDI through an Example
152. Mover Sergio; Cimatti Alessandro; Tiwari A.; Tonetta Stefano, Time-aware Relational Abstractions for Hybrid Systems
153. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, Parameter Synthesis with IC3
154. Bozzano Marco; Cimatti Alessandro; Mattarei Cristian, Efficient Analysis of Reliability Architectures via Predicate Abstraction
155. Cimatti Alessandro; Dorigatti Michele; Tonetta Stefano, OCRA: A tool for checking the refinement of temporal contracts
156. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Xavier Olive, Symbolic Synthesis of Observability Requirements for Diagnosability
157. Cimatti Alessandro; Griggio Alberto, Software Model Checking via IC3
158. Cimatti Alessandro; Raffaele Corvino; Armando Lazzaro; Narasamdya Iman; Tiziana Rizzo; Roveri Marco; Angela Sanseviero; Andrei Tchaltsev, Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
159. Cimatti Alessandro; Narasamdya Iman; Roveri Marco, Verification of Parametric System Designs
160. Cimatti Alessandro; Narasamdya Iman; Roveri Marco, Software Model Checking with Explicit Scheduler and Symbolic Threads
161. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Solving Temporal Problems using SMT: Weak Controllability
162. Cimatti Alessandro; Micheli Andrea; Roveri Marco, Solving Temporal Problems using SMT: Strong Controllability
163. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, SMT-Based Verification of Hybrid Systems
164. Cimatti Alessandro; Tonetta Stefano, A Property-Based Proof System for Contract-Based Design
165. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, Quantifier-free encoding of hybrid systems with non-linear dynamics
166. Elena Alaña; Héctor Naranjo; Yuri Yushtein; Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Régis de Ferluc; Gérard Garcia, Automated generation of FDIR for the compass integrated toolset (AUTOGEF)
167. Cimatti Alessandro; Sebastiani Roberto, Theory and Applications of Satisfiability Testing – SAT 2012
168. Cimatti Alessandro, Application of SMT solvers to hybrid system verification
169. Cimatti Alessandro; Roveri Marco; Susi Angelo; Tonetta Stefano, Validation of Requirements for Hybrid Systems: a Formal Approach
170. Robin Steel; Alexander Hoffman; Mark Niézette; Cimatti Alessandro; Roveri Marco; Konstantinos Kapellos; Alessandro Donati; Nicola Policella, Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Supporting Rover Operations Planning on Ground
171. Cavada Roberto; Cimatti Alessandro; Micheli Andrea; Roveri Marco; Susi Angelo; Tonetta Stefano, OthelloPlay: a plug-in based tool for requirement formalization and validation
172. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction
173. Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Xavier Olive, Symbolic Synthesis of Observability Requirements for Diagnosability
174. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco, Safety, Dependability and Performance Analysis of Extended AADL Models
175. Cimatti Alessandro; Mover Sergio; Roveri Marco; Tonetta Stefano, From Sequential Extended Regular Expressions to NFA with Symbolic Labels
176. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
177. Cimatti Alessandro; Narasamdya Iman; Roveri Marco, Boosting Lazy Abstraction for SystemC with Partial Order Reduction
178. Robin Steel; Alexander Hoffman; Cimatti Alessandro; Roveri Marco; Konstantinos Kapellos; Alessandro Donati; Nicola Policella, Innovative Rover Operations Concepts–Autonomous Planning: Keeping a dog on the lead
179. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, Efficient Scenario VeriFIcation for Hybrid Automata
180. Cimatti Alessandro; Griggio Alberto; Micheli Andrea; Iman Narasamdya; Roveri Marco, Kratos - A Software Model Checker for SystemC
181. Bozzano Marco; Cimatti Alessandro; Roveri Marco; Tchaltsev Andrei, A Comprehensive Approach to On-Board Autonomy Verification and Validation
182. Campana Daniele; Cimatti Alessandro; Narasamdya Iman; Roveri Marco, An Analytic Evaluation of SystemC Encodings in Promela
183. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems
184. Bozzano Marco; Cimatti Alessandro; O. Lisagor; Mattarei Cristian; Mover Sergio; Roveri Marco; Tonetta Stefano, Model Checking and Safety Assessment of Altarica models
185. Cimatti Alessandro; Susi Angelo; Tonetta Stefano; Roveri Marco, Formalizing requirements with object models and temporal constraints
186. Cimatti Alessandro; Micheli Andrea; Narasamdya Iman; Roveri Marco, Verifying SystemC: a Software Model Checking Approach
187. Anders Franzen; Cimatti Alessandro; Alexander Nadel; Sebastiani Roberto; Jonathan Shalev, Applying SMT in Symbolic Execution of Microcode
188. Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Xavier Olive, Formal Verification and Validation of AADL Model
189. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient generation of craig interpolants in satisfiability modulo theories
190. Cimatti Alessandro, SMT-Based Software Model Checking
191. Roveri Marco; Cimatti Alessandro; Narasamdya Iman; Micheli Andrea; Daniele Campana; Griggio Alberto; Tchaltsev Andrei, KRATOS
192. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco; Ralf Wimmer; Cavada Roberto, COMPASS Tool
193. Thi Thieu Hoa Le; Luigi Palopoli; Roberto Passerone; Ramadian Yusi; Cimatti Alessandro, Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study
194. Cimatti Alessandro; Anders Franzen; Griggio Alberto; Kalyanasundaram Krishnamani; Roveri Marco, Tighter Integration of BDD and SMT for Predicate Abstraction
195. Cimatti Alessandro; Anders Franzén; Griggio Alberto; Sebastiani Roberto; Cristian Stenico, Satisfiability Modulo the Theory of Costs: Foundations and Applications
196. Cimatti Alessandro; Roveri Marco; Susi Angelo; Tonetta Stefano, Formalization and Validation of Safety-Critical Requirements
197. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco; Ralf Wimmer, A Model Checker for AADL
198. Roderick Bloem; Cimatti Alessandro; Karin Greimel; Georg Hofferek; Robert Koenighofer; Roveri Marco; Schuppan Viktor; Richard Seeber, RATSY - A new Requirements Analysis Tool with Synthesis
199. Lei Bu; Cimatti Alessandro; Xuandong Li; Mover Sergio; Tonetta Stefano, Model Checking of Hybrid Systems using Shallow Synchronization
200. Angelo Chiappini; Cimatti Alessandro; Macchi Luca; Oscar Rebollo; Roveri Marco; Susi Angelo; Tonetta Stefano; Berardino Vittorini, Formalization and validation of a subset of the European Train Control System
201. Bozzano Marco; Cimatti Alessandro; Roveri Marco; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll, Codesign of Dependable Systems: A Component-Based Modeling Language
202. Roveri Marco; Cimatti Alessandro; Schuppan Viktor; Tchaltsev Andrei; Cavada Roberto, NuGAT
203. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Interpolant Generation for UTVPI
204. Cimatti Alessandro; Roveri Marco; Tonetta Stefano, Requirements Validation for Hybrid Systems
205. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version
206. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco, Codesign of Dependable Systems: A Component-Based Language
207. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco, The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
208. Cimatti Alessandro; Jori Juhani Dubrovin; Tommi Antero Junttila; Roveri Marco, Structure-Aware Computation of Predicate Abstraction
209. Dirk Beyer; Cimatti Alessandro; Griggio Alberto; Erkan Keremoglu; Sebastiani Roberto, Software Model Checking via Large-Block Encoding
210. Cavada Roberto; Cimatti Alessandro; Mariotti Alessandro; Mattarei Cristian; Micheli Andrea; Mover Sergio; Pensallorto Marco; Roveri Marco; Susi Angelo; Tonetta Stefano, Supporting Requirements Validation: The EuRailCheck Tool
211. Bozzano Marco; Cimatti Alessandro; Roveri Marco; Andrei Tchaltsev, A Comprehensive Approach to On-Board Autonomy Verification and Validation
212. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco, The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
213. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
214. Dirk Beyer; Cimatti Alessandro; Griggio Alberto; Erkan Keremoglu; Sebastiani Roberto, Software Model Checking via Large-Block Encoding
215. Bozzano Marco; Cimatti Alessandro; Roveri Marco; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll, Verification and performance evaluation of AADL models
216. Bozzano Marco; Cimatti Alessandro; Joost Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Roveri Marco, Model-Based Codesign of Critical Embedded Systems
217. Cimatti Alessandro; Bozzano Marco; Adolfo Villafiorita, FSAP
218. Cimatti Alessandro; Pistore Marco; Traverso Paolo, Automated Planning
219. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, The MathSAT 4SMT Solver
220. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, Efficient Interpolant Generation in Satisfiability Modulo Theories
221. Cimatti Alessandro; Roveri Marco; Schuppan Viktor; Tchaltsev Andrei, Diagnostic Information for Realizability
222. Cimatti Alessandro, Beyond Boolean SAT: Satisfiability Modulo Theories
223. Cimatti Alessandro; Luigi Palopoli; Ramadian Yusi, Symbolic Computation of Schedulability Regions using parametric timed automata
224. Cimatti Alessandro; Roveri Marco; Tonetta Stefano, Symbolic Compilation of PSL
225. Cimatti Alessandro; Roveri Marco; Susi Angelo; Tonetta Stefano, Object Models with Temporal Constraints
226. Cimatti Alessandro; Roveri Marco; Susi Angelo; Tonetta Stefano, From Informal Requirements to Property-Driven Formal Validation
227. Bozzano Marco; Cimatti Alessandro; Andrea Guiotto; Andrea Martelli; Roveri Marco; Tchaltsev Andrei; Yuri Yushtein, On-Board Autonomy via Symbolic Model Based Reasoning
228. Cimatti Alessandro; Andrea Guiotto; Roveri Marco, On Board Model Checking for Space Applications
229. Cimatti Alessandro; Robert B. Jones, Formal Methods in Computer-Aided Design, Portland, Oregon, USA, 17-20 November 2008
230. Bertoli Piergiorgio; Bozzano Marco; Cimatti Alessandro, A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis
231. Roberto Bruttomesso; Cimatti Alessandro; Roberto Sebasatiani; Griggio Alberto; Anders Franzen, MathSAT
232. Bozzano Marco; Cimatti Alessandro; Francesco Tapparo, Symbolic Fault Tree Analysis for Reactive Systems
233. Zvonimir Rakamaric; Bruttomesso Roberto; Alan J. Hu; Cimatti Alessandro, Verifying Heap-Manipulating Programs in an SMT Framework
234. Cimatti Alessandro; Roveri Marco; Schuppan Viktor; Tonetta Stefano, Boolean Abstraction for Temporal Logic Satisfiability
235. Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Ziyad Hanna; Alexander Nadel; Amit Palti; Sebastiani Roberto, A Lazy and Layered SMT ({BV}) Solver for Hard Industrial Verification Problems
236. Cavada Roberto; Cimatti Alessandro; Anders Franzen; Kalyanasundaram Krishnamani; Roveri Marco; R. K. Shyamasundar, Computing Predicate Abstractions by Integrating BDDs and SMT Solvers
237. Cimatti Alessandro; Griggio Alberto; Sebastiani Roberto, A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
238. Cimatti Alessandro; Roveri Marco; Tonetta Stefano, Syntactic Optimizations for PSL Verification
239. Roderick Bloem; Cimatti Alessandro; Ingo Pill; Roveri Marco, Symbolic Implementation of Alternating Automata
240. Armando Alessandro; Cimatti Alessandro, Post-workshop Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning
241. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Tommi A. Junttila; Ranise Silvio; Peter van Rossum; Sebastiani Roberto, Efficient theory combination via boolean search
242. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Anders Franzen; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Sebastiani Roberto, Encoding RTL Constructs for Mathsat: A preliminary report
243. Roderick Bloem; Cimatti Alessandro; Ingo Pill; Roveri Marco; Simone Semprini; Tchaltsev Andrei, RAT: A tool for formal analysis of requirements
244. Cimatti Alessandro; Roveri Marco; Simone Semprini; Tonetta Stefano, From PSL to NBA: a Modular Symbolic Encoding
245. Cimatti Alessandro; Sebastiani Roberto, Building Efficient Decision Procedures on top of SAT solvers
246. Armando Alessandro; Cimatti Alessandro, Preface. Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005)
247. Piergiorgio Bertoli; Cimatti Alessandro; Marco Pistore, Towards strong cyclic planning under partial observability
248. Roberto Bruttomesso; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Alessandro Santuari; Sebastiani Roberto, To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T)
249. Roberto Bruttomesso; Cimatti Alessandro; Anders Franzen; Griggio Alberto; Sebastiani Roberto, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis
250. Bertoli Piergiorgio; Cimatti Alessandro; Roveri Marco; Traverso Paolo, Strong Planning under Partial Observability
251. Marco Bernardo; Cimatti Alessandro, Formal Methods for Hardware Verification
252. R. Bloem; Cimatti Alessandro; I. Pill; Roveri Marco; S. Semprini, Symbolic Implementation of Alternating Automata
253. I. Pill; S. Semprini; Cavada Roberto; Roveri Marco; R. Bloem; Cimatti Alessandro, Formal analysis of hardware requirements
254. Bertoli Piergiorgio; Cimatti Alessandro; Pistore Marco, Strong Cyclic Planning Under Partial Observability
255. Gilles Audemard; Bozzano Marco; Cimatti Alessandro; Sebastiani Roberto, Verifying Industrial Hybrid Systems with MathSAT
256. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Tommi Junttila; Peter van Rossum; Stephan Schulz; Sebastiani Roberto, Mathsat: Tight Integration of SAT and Mathematical Decision Procedures
257. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Tommi Junttila; Ranise Silvio; Peter van Rossum; Sebastiani Roberto, Efficient Satisfiability Modulo Theories via Delayed Theory Combination
258. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; T. A. Junttila; Rossum Peter Van; S. P. Schulz; Sebastiani Roberto, An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic
259. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Tommi A. Junttila; Peter van Rossum; Stephan Peter Schulz; Sebastiani Roberto, The Mathsat3 System
260. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; T. Antero Junttila; Ranise Silvio; Rossum Peter Van; Sebastiani Roberto, Efficient Theory Combination via Boolean Search
261. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; T. A. Junttila; R. Peter van; S. P. Schulz; Sebastiani Roberto, MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures
262. Bozzano Marco; R. Brutomesso; Cimatti Alessandro; T. A. Junttila; Ranise Silvio; Rossen Peter Van; Sebastiani Roberto, Efficient Satisfiability Modulo Theories via Delayed Theory Combination
263. Roveri Marco; Cimatti Alessandro; Tchaltsev Andrei; Cavada Roberto; Simone Semprini; Roderick Bloem; Ingo Pill, RAT
264. Bertoli Piergiorgio; Cimatti Alessandro; Traverso Paolo, Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains
265. Bozzano Marco; Cimatti Alessandro; Gabriele Colombini; Veselin Kirov; Sebastiani Roberto, The MathSAT solver -- a progress report
266. Cimatti Alessandro; Roveri Marco; Bertoli Piergiorgio, Conformant Planning via Symbolic Model Checking and Heuristic Search
267. Cimatti Alessandro; Roveri Marco; D. Sheridan, Bounded Verification of Past LTL
268. Bozzano Marco; Cimatti Alessandro; G. Colombini; V. Kirov; Sebastiani Roberto, The MAthSAT Solver. A progress report
269. Bozzano Marco; Bruttomesso Roberto; Cimatti Alessandro; Sebastiani Roberto, The MathSAT Solver - a comparative evaluation
270. Roelofsen Floris; Serafini Luciano; Cimatti Alessandro, Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems
271. Bertoli Piergiorgio; Cimatti Alessandro; Lago U. Dal; Pistore Marco, Extending PDDL to nondeterminism, limited sensing and iterative conditinal plans
272. Benedetti Marco; Cimatti Alessandro, Bounded Model Checking for past LTL
273. Cimatti Alessandro; Charles Pecheur; Cavada Roberto, Formal Verification of Diagnosability via Symbolic Model Checking
274. Armin Biere; Cimatti Alessandro; E. M. Clarke; Ofer Strichman; Yunshan Zhu, Bounded Model Checking
275. Audemard Gilles; Bozzano Marco; Cimatti Alessandro; Sebastiani Roberto, Verifying Industrial Hybrid Systems with MathSAT
276. Cimatti Alessandro; Pistore Marco; Roveri Marco; Traverso Paolo, Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking
277. Bertoli Piergiorgio; Cimatti Alessandro; Pistore Marco; Traverso Paolo, A Framework for Planning with Extended Goals under Partial Observability
278. Bertoli Piergiorgio; Cimatti Alessandro; Lago U. Dal; Pistore Marco, Extending PDDL to mondeterminism, limited sensing and iterative conditional plans
279. Bozzano Marco; Villafiorita Monteleone Adolfo; O. Akerlund; P. Bieber; C. Bougnol; E. Boede; M. Bretschneider; A. Cavallo; C. Castel; M. Cifaldi; Cimatti Alessandro; A. Griffault; C. Kehren; B. Lawrence; A. Luedtke; S. Metge; C. Papadopoulos; R. Passarello; T. Peikenkamp; P. Persson; C. Seguin; L. Trotta; L. Villafiorita A. Valacca; Zacco Gabriele, ESACS: an integrated methodology for design and safety analysis of complex systems
280. Bertoli Piergiorgio; Cimatti Alessandro; Traverso Paolo, Interleaving Execution and Planning via Symbolic Model Checking
281. Bertoli Piergiorgio; Cimatti Alessandro; Pistore Marco; Roveri Marco; Traverso Paolo, MBP: A Model Based Planner
282. Cimatti Alessandro; C. Pecheur; Cavada Roberto, Formal Verification of Diagnosability via Symbolic Model Checking
283. Roveri Marco; Cimatti Alessandro; Cavada Roberto; Tchaltsev Andrei; Micheli Andrea; Mariotti Alessandro; Mover Sergio; Marco Pensallorto; Armando Tacchella; Daniel Sheridan; Gavin Keighren; Tommi Junttila; Timo Latvala, NuSMV
284. Cimatti Alessandro; Pistore Marco; Roveri Marco; Sebastiani Roberto, Improving the encoding of LTL Model Checking into SAT
285. Audemard Gilles; Cimatti Alessandro; Kornilowicz Artur; Sebastiani Roberto, Bounded Model Checking for Timed Systems
286. Cimatti Alessandro; E. Giunchiglia; Roveri Marco; Pistore Marco; Sebastiani Roberto; A. Tacchella, Integrating BDD-based and SAT-based Symbolic Model Checking
287. Bertoli Piergiorgio; Cimatti Alessandro; J. Slaney; S. Thiebaux, Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking
288. Audemard Gilles; Bertoli Piergiorgio; Cimatti Alessandro; Kornilowicz Artur; Sebastiani Roberto, A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions
289. Audemard Gilles; Bertoli Piergiorgio; Cimatti Alessandro; Kornilowicz Artur; Sebastiani Roberto, Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements
290. Cimatti Alessandro; E. M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Pistore Marco; Roveri Marco; Roberto Sebastiani; A. Tacchella, NuSMV 2: An OpenSource Tool for Symbolic model Checking
291. Bertoli Piergiorgio; Cimatti Alessandro; Pistore Marco; Traverso Paolo, Plan Validation for Extended Goals under Partial Observability (preliminary report)
292. Cimatti Alessandro; Roveri Marco; Bertoli Piergiorgio, Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking
293. Cimatti Alessandro, Industrial Applications of Model Checking
294. Bertoli Piergiorgio; Cimatti Alessandro; Roveri Marco, Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning
295. Cimatti Alessandro; E. Giunchiglia; Pistore Marco; Roveri Marco; Sebastiani Roberto; A. Tacchella, NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking
296. Bertoli Piergiorgio; Cimatti Alessandro; Roveri Marco, Conditional Planning under Partial Obserbability as Heuristic-Symbolic Search in Belief Space
297. Bertoli Piergiorgio; Cimatti Alessandro; Roveri Marco; Traverso Paolo, Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking
298. Massimo Benerecetti; Cimatti Alessandro, Symbolic model checking for multi-agent systems
299. Bertoli Piergiorgio; Cimatti Alessandro; Pistore Marco; Roveri Marco; Traverso Paolo, MBP: a Model Based Planner
300. Bertoli Piergiorgio; Cimatti Alessandro, Improving Heuristics for Planning and Search in Belief Space
301. Cimatti Alessandro; Serafini Luciano, A Context-Based Mechanization of Multi-Agent Reasoning
302. Cimatti Alessandro; Roveri Marco, Forward Conformant Planning via Symbolic Model Checking
303. V. Hartonas Garmhausen; E. M. Clarke; S. Campos; Cimatti Alessandro; Giunchiglia Fausto, Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints
304. Cimatti Alessandro; E. M. Clarke; Giunchiglia Fausto; Roveri Marco, NuSMV: a new symbolic model checker
305. Cimatti Alessandro; Roveri Marco, Conformant Planning via Model Checking
306. Bertoli Piergiorgio; Cimatti Alessandro; Traverso Paolo, Integrating Formal Methods into the Development Cycle of a Safety-critical Embedded Software System
307. Cimatti Alessandro; Roveri Marco, Conformant Planning via Symbolic Model Checking
308. Cimatti Alessandro; E. M. Clarke; Fausto Giunchiglia; Roveri Marco, NuSMV: a New Symbolic Model Verifier
309. Cimatti Alessandro; P. L. Pieraccini; Sebastiani Roberto; Traverso Paolo; Villafiorita Monteleone Adolfo, Formal Specification and validation of a Vital Communication Protocol
310. A. Chiappini; Cimatti Alessandro; C. Porzia; G. Rotondo; Sebastiani Roberto; Traverso Paolo; Villafiorita Monteleone Adolfo, Formal Specification and Development of a Safety-Critical Train Management
311. Cimatti Alessandro; Roveri Marco, Conformant Planning via Model Checking
312. Cimatti Alessandro; Giunchiglia Fausto; Traverso Paolo; Villafiorita Monteleone Adolfo, Run-Time Result Formal Verification of Safety Critical Software: an Industrial Case Study
313. Cimatti Alessandro; Giunchiglia Fausto; R. W. Weyhrauch, A Many Sorted Natural Deduction
314. Cimatti Alessandro; E. M. Clarke; Giunchiglia Fausto; Roveri Marco, NuSMV: A Reimplementation of SMV
315. Cimatti Alessandro; Roveri Marco; Traverso Paolo, Strong Planning in Non-Deterministic Domains via Model Checking
316. Cimatti Alessandro; Roveri Marco; Traverso Paolo, Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains
317. Cimatti Alessandro; Sebastiani Roberto, Servizi forniti dagli strati Safety Layer e Connection Manager
318. Cimatti Alessandro; Sebastiani Roberto, Specifica formale dei protocolli Safety Layer e Connection Manager
319. Cimatti Alessandro; Sebastiani Roberto, Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL
320. Bertoli Piergiorgio; Cimatti Alessandro; Giunchiglia Fausto; Traverso Paolo, A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools
321. Cimatti Alessandro; Giunchiglia Fausto; Roveri Marco, Abstraction in Planning via Model Checking
322. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; D. Romano; F. Torielli; Traverso Paolo, Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System
323. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; D. Romano; F. Torielli; Traverso Paolo, Formal Verification of a Railway Interlocking System Using Model Checking
324. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Traverso Paolo, Formal Validation of an Interlocking System for Large Railway Stations: A Case Study
325. Cimatti Alessandro; Giunchiglia Fausto; P. Pecchiari; B. Pietra; J. Profeta; D. Romano; Traverso Paolo; B. Yu, A Provably Correct Embedded Verifier for the Certification of Safety Critical Software
326. Cimatti Alessandro; Enrico Giunchiglia; Giunchiglia Fausto; Traverso Paolo, A Model Based Decision Procedure for Common Sense Temporal Reasoning
327. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; D. Romano; F. Torielli; Traverso Paolo, Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System
328. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; B. Pietra; D. Romano; F. Torielli; Traverso Paolo, Formal Validation & Verification of Software for Railway Control and Protection Systems: Experimental Applications in ANSALDO
329. Bertoli Piergiorgio; Cimatti Alessandro; Giunchiglia Fausto; Traverso Paolo, Certification of Translators via Off-line and On-line Proof Logging and Checking
330. Cimatti Alessandro; Enrico Giunchiglia; Giunchiglia Fausto; Traverso Paolo, Planning via Model Checking: A Decision Procedure for AR
331. Bouquet Paolo; Cimatti Alessandro, Mechanizing Local Reasoning with Contexts
332. Cimatti Alessandro; Serafini Luciano, Mechanizing Multi-Agent Reasoning with Belief Contexts
333. Massimo Benerecetti; Cimatti Alessandro; Enrico Giunchiglia; Giunchiglia Fausto; Serafini Luciano, Context-Based Formal Specification of Multi-Agent Systems
334. Cimatti Alessandro; Traverso Paolo, Computational Reflection via Mechanized Logical Deduction
335. Enrico Giunchiglia; Armando Alessandro; Traverso Paolo; Cimatti Alessandro, Visual Representation of Natural Language Scene Descriptions
336. Giuliano Antoniol; Caprile Bruno Giovanni; Cimatti Alessandro; Roberto Fiutem, Experiencing Real-Life Interactions with the Mobile Platform of MAIA
337. Cimatti Alessandro; Serafini Luciano, Multi-Agent Reasoning with Belief Contexts III: Towards the Mechanization
338. Cimatti Alessandro; Serafini Luciano, Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study
339. Cimatti Alessandro; Serafini Luciano, Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance
340. Armando Alessandro; Cimatti Alessandro; E. Giunchiglia; P. Pecchiari; L. Spalazzi; Traverso Paolo, Flexible Planning by Integrating Multilevel Reasoning
341. Traverso Paolo; Cimatti Alessandro; Luca Spalazzi; Enrico Giunchiglia; Armando Alessandro, MRG: Building planners for real world complex applications
342. Giunchiglia Fausto; Armando Alessandro; Cimatti Alessandro; Traverso Paolo, First steps towards provably correct system synthesis of system code
343. Cimatti Alessandro; Giunchiglia Fausto; G. Mongardi; D. Romano; F. Torielli; Traverso Paolo, Valutazione del CBR-tool orientato all`help desk `Case Advisor`
344. Giunchiglia Fausto; Traverso Paolo; Cimatti Alessandro; Luca Spalazzi; Sandro Dalbosco; Serafini Luciano; Enrico Giunchiglia; Alessandro Armando; Paolo Pecchiari, MRG: sistema di ragionamento
345. Giunchiglia Fausto; Traverso Paolo; Cimatti Alessandro; Luca Spalazzi; Sandro Dalbosco; Serafini Luciano; Enrico Giunchiglia; Armando Alessandro; Paolo Pecchiari, MRG: un nucleo di ragionamento per un sistema integrato multifunzionale
346. Traverso Paolo; Luca Spalazzi; Cimatti Alessandro, A planning language and a semantics for real world autonomous agents
347. Traverso Paolo; Cimatti Alessandro; Luca Spalazzi, Beyond the single planning paradigm: introspective planning
348. Luca Spalazzi; Cimatti Alessandro; Traverso Paolo, Implementing planning as tactical reasoning
349. Traverso Paolo; Cimatti Alessandro; Luca Spalazzi; Enrico Giunchiglia, Building planners with explicit control mechanism
350. Cimatti Alessandro; Traverso Paolo; Luca Spalazzi, Programming Planners with Flexible Architectures
351. Cimatti Alessandro; Traverso Paolo; Sandro Dalbosco; Armando Alessandro, Navigation by Combining Reactivity and Planning
352. Giunchiglia Fausto; Traverso Paolo; Cimatti Alessandro; Paolo Pecchiari, A System for Multi-Level Reasoning
353. Giunchiglia Fausto; Traverso Paolo; Cimatti Alessandro; Luca Spalazzi, Tactics: extending the notion of plan
354. Giunchiglia Fausto; Traverso Paolo; Cimatti Alessandro; Luca Spalazzi; Sandro Dalbosco; Serafini Luciano; Enrico Giunchiglia; Armando Alessandro; Paolo Pecchiari, Un nucleo di ragionamento per un sistema integrato multi-funzionale: stato di avanzamento
355. Giunchiglia Fausto; Cimatti Alessandro; Sandro Dalbosco; Traverso Paolo; Luca Spalazzi, MRG: un sistema di ragionamento distribuito per applicazioni complesse