You are here
Marco Bozzano
Researcher
 Email:
 Phone: 0461314367
 FBK Povo
Short bio
Graduated in Computer Science  University of Genova (1997)
PhD in Computer Science  DISI, University of Genova (2002)
Reasercher at Fondazione Bruno Kessler (from 2002)
Research interests
Formal Methods
Symbolic Model Checking
Formal Safety Assessment
Logic Programming
Linear Logic
Personal documents
Related projects
Publications
2016

Bittner, Benjamin; Bozzano, Marco; Cavada, Roberto; Cimatti, Alessandro; Gario, Marco; Griggio, Alberto; Mattarei, Cristian; Micheli, Andrea; Zampedri, Gianni,Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,vol.9636,2016, pp. 533539, (Tools and Algorithms for the Construction and Analysis of Systems,Eindhoven, The Netherlands,28 aprile 2016)

Benjamin, Bittner; Marco, Bozzano; Alessandro, Cimatti; Gianni, Zampedri,Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI 2016),2016, pp. 907913, (30th AAAI Conference on Artificial Intelligence (AAAI 2016),Phoenix, Arizona, Stati Uniti,12–17/02/2016)

Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro,Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI,2016, pp. 972978, (25th International Joint Conference on Artificial Intelligence,New York City, NY, Stati Uniti,915 July 2016)
2015

Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta,Safety Assessment of AltaRica Models via Symbolic Model Checking,in «SCIENCE OF COMPUTER PROGRAMMING»,vol. 98,2015, pp. 464 483

Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano,in «LOGICAL METHODS IN COMPUTER SCIENCE»,vol. 11,n. 4,2015

Bozzano M.; Cimatti A.; Gario M.; Micheli A.,SMTbased Validation of Timed Failure Propagation Graphs,Proceedings of the 29th AAAI Conference on Artificial Intelligence,Palo Alto, California,AAAI Press,2015, (AAAI 2015,Austin, Texas, USA,25/01/2015  30/01/2015)

Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian,Computer Aided Verification  27th International Conference, CAV 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part I,vol.9206,2015, pp. 603621, (27th International Conference on Computer Aided Verification, CAV 2015,San Francisco, CA,July 1824, 2015)

Bozzano, M.; Cimatti, A.; Fernandes Pires, A.; Jones, D.; Kimberly, G.; Petri, T.; Robinson, R.; Tonetta, S.,Computer Aided Verification  27th International Conference, CAV 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part I,vol.9206,2015, pp. 518535, (27th International Conference on Computer Aided Verification (CAV),San Francisco, CA, USA,July 1824, 2015)
2014

Bozzano M.; Cimatti A.; Katoen J.P.; Katsaros P.; Mokos K.; Nguyen V.Y.; Noll T.; Postma B.; Roveri M.,Spacecraft Early Design Validation using Formal Methods,in «RELIABILITY ENGINEERING & SYSTEM SAFETY»,vol. 132,2014, pp. 20 35

Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic,TACAS 2014, LNCS 8413,,Berlin,SpringerVerlag,vol.8413,2014, pp. 326340, (Tools and Algorithms for the Construction and Analysis of Systems  20th International Conference, TACAS 2014,Grenoble, Francia,2014)

M. Bozzano; A. Cimatti; C. Mattarei; S. Tonetta,Formal Safety Assessment via ContractBased Design.,ATVA14,2014, pp. 8197, (Automated Technology for Verification and Analysis,Sydney,

Bittner B.; Bozzano M.; Cimatti A.; Gario M.; Griggio A.,Towards ParetoOptimal Parameter Synthesis for Monotonic Cost Functions,Proceedings of the 14th Conference on Formal Methods in ComputerAided Design,2014, pp. 2330

Guiotto A.; De Ferluc R.; Bozzano M.; Cimatti A.; Gario M.; Yushtein Y.,FAME Process: A Dedicated Development and V&V Process for FDIR,ESA SP725,2014, (DASIA 2014,Warsaw, Poland,June 3rd  June 5th)

Bittner B.; Bozzano M.; Cimatti A.; De Ferluc R. ; Gario M.; Guiotto A. ; Yushtein Y.,An Integrated Process for FDIR Design in
Aerospace,LNCS 8822,Springer International Publishing,vol.8822,2014, pp. 8295, (International Symposium on Model Based Safety and Assessment,Munich, Germany,October 2729, 2014) 
Bittner B.; Bozzano M. ; Cimatti A.; De Ferluc R.; Gario M.; Guiotto A.; Yushtein Y.,FAME: A ModelBased Environment for FDIR Design in Aerospace,Proceedings of the International Symposium on Model Based Safety and Assessment,Springer International Publishing,vol.8822,2014, pp. 12, (International Symposium on Model Based Safety and Assessment,Munich, Germany,October 2729, 2014)
2013

R. Banach; M. Bozzano,The Mechanical Generation of Fault Trees for Reactive Systems via Retrenchment I: Combinational Circuits,in «FORMAL ASPECTS OF COMPUTING»,vol. 25,n. 4,2013, pp. 573 607

R. Banach; M. Bozzano,The Mechanical Generation of Fault Trees for Reactive Systems via Retrenchment II: Clocked and Feedback Circuits,in «FORMAL ASPECTS OF COMPUTING»,vol. 25,n. 4,2013, pp. 609 657

Marco Bozzano; Adolfo Villafiorita,in Encyclopedia of Software Engineering,New York,CRC Press, Taylor & Francis Group,2013

Marco Bozzano; Alessandro Cimatti; Cristian Mattarei,Automated Analysis of Reliability Architectures,18th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2013, Singapore, July 1719, 2013,IEEE Computer Society,2013, pp. 198207, (International Conference on Engineering of Complex Computer Systems,Singapore,07/17/2013 07/19/2013)

Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,AAAI Workshops,2013, (Workshops at the TwentySeventh AAAI Conference on Artificial Intelligence,Bellevue, Washington, USA,14–18 July 2013)

Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,Formal Specification and Synthesis of FDI through an Example,Proceedings of the 24th International Workshop on Principles of Diagnosis,2013, (The 24th International Workshop on Principles of Diagnosis,Jerusalem, Israel,October 14, 2013)

Marco Bozzano; Alessandro Cimatti; Cristian Mattarei,Efficient Analysis of Reliability Architectures via Predicate Abstraction,Hardware and Software: Verification and Testing  9th International Haifa Verification Conference,Springer,vol.8244,2013, pp. 279294, (Ninth Haifa Verification Conference,Haiva, Israel,5  7 November 2013)
2012

Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive,Symbolic Synthesis of Observability Requirements for Diagnosability,Proceedings of the TwentySixth AAAI Conference on Artificial Intelligence,AAAI Press,2012, (AAAI 2012: TwentySixth AAAI Conference on Artificial Intelligence,Toronto, Canada,da 07/22/2012 a 07/26/2012)

Elena Alaña; Héctor Naranjo; Yuri Yushtein; Marco Bozzano; Alessandro Cimatti; Marco Gario; Régis de Ferluc; Gérard Garcia,Automated generation of FDIR for the compass integrated toolset (AUTOGEF),2012, (DASIA 2012,Dubrovnik, Croatia,14/05/2012  16/05/2012)
2011

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,Safety, Dependability and Performance Analysis of Extended AADL Models,in «COMPUTER JOURNAL»,vol. 54,n. 5,2011, pp. 754 775

Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,A Comprehensive Approach to OnBoard Autonomy Verification and Validation,AAAI (Conference on Artificial Intelligence)
Press,2011, (IJCAI 2011,Barcelona, Catalonia (Spain),1622/07/2011) 
M. Bozzano; A. Cimatti; O. Lisagor; C. Mattarei; S. Mover; M. Roveri; S. Tonetta,Model Checking and Safety Assessment of Altarica models,in «ELECTRONIC COMMUNICATIONS OF THE EASST»Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011),Berlin,EASST,vol.46,2011, (AVOCS 2011  11th International Workshop on Automated Verification of Critical Systems,Newcastle, UK,da 09/12/2011 a 09/14/2011)

Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive,Symbolic Synthesis of Observability Requirements for Diagnosability,Proceedings of 11th Symposium on Advanced Space Technologies in Robotics and Automation,Noordwijk,2011, (ASTRA 2011,Noordwijk, The Netherlands,12/04/2011 – 14/04/2011)
2010

Marco Bozzano; Adolfo Villafiorita,Design and Safety Assessment of Critical Systems,London,Auerbach Publications (Taylor & Francis Group),2010

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer,A Model Checker for AADL,Proceedings of 22nd International Conference on Computer Aided Verification,Springer,vol.6174,2010, pp. 562565, (CAV 2010,Edinburgh, UK,1519/07/2010)

Marco Bozzano; Roberto Cavada; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Xavier Olive,Formal Verification and Validation of AADL Model,2010, (ERTS² 2010  Embedded Real Time Software and Systems,Toulouse, France,1921/05/2010)

Oleg Lisagor; Marco Bozzano; Matthias Bretschneider; Tim Kelly,Incremental Safety Assessment: Enabling the Comparison of Safety Analysis Results,2010, (ISSC10  28th International System Safety Conference,Minneapolis, Minnesota,30/0803/09/2010)

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer; Roberto Cavada,2010,
2009

Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,Workshop on Verification and Validation of Planning and Scheduling Systems,2009, pp. 110, (VV&PS 2009  ICAPS,Thessaloniki, Greece,20/09/2009)

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,Proceedings of 28th Int. International Conference on Computer Safety, Reliability and Security,Springer,vol.5775,2009, pp. 173186, (SAFECOMP 2009,Hamburg, Germany,1518/09/2009)

Marco Bozzano; Alessandro Cimatti; Marco Roveri; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll,Verification and performance evaluation of AADL models,Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering,New York,ACM,2009, pp. 285286, (ESEC/FSE 2009,Amsterdam, The Netherlands,2428/08/2009)

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,Proceedings 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems,CEURWS.org,vol.507,2009, pp. 8791, (ACESMB09,Denver, Colorado, USA,06/10/2009)

Marco Bozzano; Alessandro Cimatti; Marco Roveri; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll,Codesign of Dependable Systems: A ComponentBased Modeling Language,Proceedings of the 7th IEEE/ACM Int. Conference on Formal Methods and Models for Codesign,Piscataway, NJ,2009, pp. 121130, (MEMOCODE'09,Cambridge, Massachusetts, USA,1315/07/2009)

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,Codesign of Dependable Systems: A ComponentBased Language,2009

Marco Bozzano; Alessandro Cimatti; JoostPieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,2009
2008

Marco Bozzano; Alessandro Cimatti; Andrea Guiotto; Andrea Martelli; Marco Roveri; Andrei Tchaltsev; Yuri Yushtein,OnBoard Autonomy via Symbolic Model Based Reasoning,Proceedings of 10th Workshop on Advanced Space Technologies for Robotics and Automation,Noordwijk,2008, (ASTRA 2008,Noordwijk, The Netherlands,11/11/2008  13/11/2008)

Alessandro Cimatti; Marco Bozzano; Adolfo Villafiorita,FSAP,2008,
2007

Marco Bozzano; Adolfo Villafiorita,The FSAP/NuSMVSA Safety Analysis Platform,in «INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER»,vol. 9,n. 1,2007, pp. 5 24

Piergiorgio Bertoli; Marco Bozzano; Alessandro Cimatti,A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis,Model Checking and Artificial Intelligence,Berlin, Heidelberg,SpringerVerlag,2007, pp. 1 18

Marco Bozzano; Alessandro Cimatti; Francesco Tapparo,Symbolic Fault Tree Analysis for Reactive Systems,5th Int. Symposium on Automated Technology for Verification and Analysis,SpringerVerlag,vol.4762,2007, pp. 162176, (ATVA 2007,Tokyo, Japan,2225/10/2007)
2006

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,Efficient theory combination via boolean search,in «INFORMATION AND COMPUTATION»,vol. 204,n. 10,2006, pp. 1493 1525

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzen; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani,Proceedings of 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,vol.144, issue 2,2006, pp. 314, (PDPAR 2005 affiliated workshop to CAV'05,University of Edinburgh, Scotland, UK,12/07/2005)

Richard Banach; Marco Bozzano,Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems,International Conference on Computer Safety, Security and Reliability,n. 4166,2006, pp. 127141, (SAFECOMP 2006,Gdansk, Poland,2629/09/2006)

O. Akerlund; P. Bieber; E. Boede; M. Bozzano; M. Bretschneider; C. Castel; A. Cavallo; M. Cifaldi; J. Gauthier; A. Griffault; O. Lisagor; A. Luedtke; S. Metge; C. Papadopoulos; T. Peikenkamp; L. Sagaspe; C. Seguin; H. Trivedi; L.Valacca.,ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects.,2006, (ERTS’06  Embedded Real Time Software,Toulouse, France,2527/01/2006)
2005

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Peter van Rossum; Stephan Schulz; Roberto Sebastiani,Mathsat: Tight Integration of SAT and Mathematical Decision Procedures,in «JOURNAL OF AUTOMATED REASONING»,vol. 35,n. 13,2005, pp. 265 293

M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; Rossum Peter van; S. P. Schulz; R. Sebastiani,An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic,Proceedings of 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,Springer,vol.3440,2005, pp. 317333, (TACAS 2005,Edinburgh, UK,04/04/2005  08/04/2005)

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Peter Schulz; Roberto Sebastiani,The Mathsat3 System,Proceedings of 20th Int. Conference on Automated Deduction,Springer,vol.3632,2005, pp. 315321, (CADE20,Tallin, Estonia,2227/07/2005)

Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,Verifying Industrial Hybrid Systems with MathSAT,Proceedings of 2nd Int. Workshop on Bounded Model Checking,Elsevier B.V.,vol.119, issue 2,2005, pp. 1732, (BMC 2004,Boston, MA, USA,18/07/2004)

Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani,Efficient Satisfiability Modulo Theories via Delayed Theory Combination,Proceeding of 17th Int. Conference on Computer Aided Verification,Springer,vol.3576,2005, pp. 335349, (CAV,University of Edinburgh, Scotland, UK,610/07/2005)

M. Bozzano; R. Bruttomesso; A. Cimatti; T. Antero Junttila; S. Ranise; Rossum Peter van; R. Sebastiani,Efficient Theory Combination via Boolean Search,Many approaches to the decision of quantifier free formulae with respect to a background theory T  also known as Satisfiability Modulo Theory, or SMT(T)  rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory is the combination T1 U T2 of two simpler theories, the approach is typically instantiated by means of a combination schema (e.g. NelsonOppen, Shostak).
In this paper we propose a new approach to SMT(T1 U T2), where the enumerator of truth assignments is integrated with two decision procedures for T1 and for T2, which act independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the purified formula, but also to all the equalities between interface variables.
This approach is simple and expressive: for instance, no modification is required to handle nonconvex theories (as opposed to traditional NelsonOppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on stateoftheart boolean and SMT search techniques, and on theory layering (i.e. cheaper reasoning first, and more often).
We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (EUF) and Linear Arithmetic (LA), both for (the convex case of) reals and for (the nonconvex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with competitor tools, obtaining speedups up to two orders of magnitude,2005 
M. Bozzano; R. Bruttomesso; A. Cimatti; T. A. Junttila; R. Peter van; S. P. Schulz; R. Sebastiani,MathSAT: Thigt Integration of SAT and Mathematical Decision Procedures,Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard realworld problems (e.g. modelchecking, circuit testing, propositional planning) by encoding into SAT.
However, a purely boolean representation is not expressive enough for many other realworld applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in Linear Arithmetic Logic (LAL), i.e., the boolean combination of propositional variables and linear constraints over numerical variables.
In this paper we present mathsat, a new, SATbased decision procedure for LAL, based on the (known approach) of integrating a stateoftheart SAT solver with a dedicated mathematical solver for LAL. We improve mathsat in two different directions.
First, the top level procedure is enhanced, and now features a tighter integration between the boolean search and the mathematical solver. In particular, we allow for theorydriven backjumping and learning, and theorydriven deduction; we use static learning in order to reduce the number of boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stackbased interface that allows us to implement mathematical reasoning in an incremental and backtrackable way.
Second, the mathematical solver is based on layering, i.e. the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes calls of the subsequent solvers superfluous.
We provide a thorough experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several stateoftheart decision procedures. We show that the behavior of mathsat is often superior to its competitors, both on LAL, and in the subclass of Difference Logic,2005 
M. Bozzano; R. Brutomesso; A. Cimatti; T. A. Junttila; S. Ranise; Rossen Peter van; R. Sebastiani,Efficient Satisfiability Modulo Theories via Delayed Theory Combination,The problem of deciding the satisfiability of a quantifierfree formula with respect to a background theory, also known as Satisfiability Modulo Theories (smt), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of realworld problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems).
In this paper, we focus on the case where the background theory is the combination T1 U T2 of two simpler theories. Many smt procedures combine a boolean model enumeration with a decision procedure for T1 U T2, where conjunctions of literals can be decided by an integration schema such as NelsonOppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise).
We propose a new approach for SMT(T1 U T2), called Delayed Theory Combination, which does not require a decision procedure for T1 U T2, but only individual decision procedures for T1 and T2, which are directly integrated to the boolean model enumerator.
This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of nonconvex theories.
We show the effectiveness of the approach by a thorough experimental comparison,2005
2004

M. Bozzano; G. Delzanno; M. Martelli,Model Checking Linear Logic Specifications,in «THEORY AND PRACTICE OF LOGIC PROGRAMMING»,vol. 4,n. 56,2004, pp. 573 619

M. Bozzano; G. Delzanno,Automatic Verification of Secrecy Properties for Linear Logic Specifications of Cryptographic Protocolos,in «JOURNAL OF SYMBOLIC COMPUTATION»,vol. 38,n. 5,2004, pp. 1375 1415

Marco Bozzano; Alessandro Cimatti; Gabriele Colombini; Veselin Kirov; Roberto Sebastiani,The MathSAT solver  a progress report,Proceeding of 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning,2004, (PDPAR,University College Cork, Ireland,05/07/2004)

M. Bozzano; A. Cimatti; G. Colombini; V. Kirov; R. Sebastiani,The MAthSAT Solver. A progress report,Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest.
The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that ``more expensive'' layers are called less frequently.
In this paper, we show the advances in the development of MathSat. We discuss the implications related to the use of Minisat, a newgeneration propositional SAT solver; the role of an incremental mathematical reasoner; the role of static learning; and the extension to integer variables. We show that the new version of MathSat is significantly more efficient than the previous one,2004 
Marco Bozzano; R. Bruttomesso; A. Cimatti; R. Sebastiani,The MathSAT Solver  a comparative evaluation,Many problems of practical relevance are conveniently expressed as boolean combinations of propositional variables and mathematical constraints. The development of decision procedures able to check the satisfiability of such formulas is therefore being devoted an increasing interest. The MathSat family of deciders is based on the extension of a DPLL propositional satisfiability procedure, used as an assignment enumerator. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power (e.g. to reason about equality and linear arithmetic) in such a way that "more expensive" layers are called less frequently.
In this paper, we discuss the advances in the development of MathSat. In particular, the current version of the tool is built on minisat, a newgeneration propositional SAT solver, and Cassowary, an incremental mathematical reasoner, and it incorporates support for integer variables. We compare the performance of MathSat with CVCL and show that MathSat is significantly more efficient on a set of benchmarks related to wordlevel verification,2004
2003

Marco Bozzano; Adolfo Villafiorita,Integrating Fault Tree Analysis with Event Ordering Information,:Safety & Reliability  ESREL 2003  Proceedings of the European Safety and Reliability Conference 2003,2003, (:Safety & Reliability  ESREL 2003  Proceedings of the European Safety and Reliability Conference 2003,2003)

Marco Bozzano; Adolfo Villafiorita; O. Akerlund; P. Bieber; C. Bougnol; E. Boede; M. Bretschneider; A. Cavallo; C. Castel; M. Cifaldi; Alessandro Cimatti; 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; Gabriele Zacco,ESACS: an integrated methodology for design and safety analysis of complex systems,Safety & Reliability  ESREL 2003  Proceedings of the European Safety and Reliability Conference 2003,Balkema,2003, (Safety & Reliability  ESREL 2003  Proceedings of the European Safety and Reliability Conference 2003,Maastricht, The Netherlands,2003)

Marco Bozzano; Adolfo Villafiorita,Improving System Reliability via Model Checking: the FSAP/NuSMVSA Safety Analysis Platform,Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,2003, pp. 4962, (Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,2003)

Marco Bozzano; A. Cavallo; M. Cifaldi; L. Valacca; Adolfo Villafiorita,Improving Safety Assessment of Complex Systems: An Industrial case study,FME 2003: Formal Methods. Proceedings of the International Symposium of Formal Methods,2003, pp. 208222, (FME 2003: Formal Methods. Proceedings of the International Symposium of Formal Methods,2003)

Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,CADE19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),2003, pp. 6276, (CADE19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),Miami, USA,2003)

Marco Bozzano; Adolfo Villafiorita,Improving System Reliability via Mdel Checking: the FSAP/NuSMVSA Safety Analysis Platform,Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMVSA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMVSA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and nonmonotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analysis for Complex Systems), an EuropeanUnionsponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development,2003

Marco Bozzano; A. Cavallo; M. Cifaldi; L. Valacca; Adolfo Villafiorita,Improving Safety Assessment of Complex Systems: An Industrial case study,The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a EuropeanUnionsponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform  the ESACS platform  that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft,2003
2002

Bozzano, Marco; Delzanno, Giorgio; Martelli, Maurizio,An effective fixpoint semantics for linear logic programs,in «THEORY AND PRACTICE OF LOGIC PROGRAMMING»,vol. 2,n. 01,2002, pp. 85 122

Marco Bozzano; G. Delzanno,Automated Protocol Verification in Linear Logic,Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming [PPDP 2002],2002

Bozzano, Marco; Delzanno, Giorgio,Beyond parameterized verification,International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems,Heidelberg,Springer,vol.2280,2002, pp. 221235, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems,Grenoble, France,April 8–12, 2002)

Bozzano, Marco; Delzanno, Giorgio,Algorithmic Verification of InvalidationBased Protocols,Computer Aided Verification,Heidelberg,Spinger,vol.2404,2002, pp. 295308, (14th International Conference, CAV 2002,Copenhagen, Denmark,July 27–31, 2002)