You are here

Marco Bozzano

Researcher
  • 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
Publications

2016

  1. 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. 533-
    539
    , (Tools and Algorithms for the Construction and Analysis of Systems,
    Eindhoven, The Netherlands,
    2-8 aprile 2016)
  2. Benjamin, Bittner; Marco, Bozzano; Alessandro, Cimatti; Gianni, Zampedri,
    Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI 2016),
    2016
    , pp. 907-
    913
    , (30th AAAI Conference on Artificial Intelligence (AAAI 2016),
    Phoenix, Arizona, Stati Uniti,
    12–17/02/2016)
  3. Bittner, Benjamin; Bozzano, Marco; Cimatti, Alessandro,
    Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI,
    2016
    , pp. 972-
    978
    , (25th International Joint Conference on Artificial Intelligence,
    New York City, NY, Stati Uniti,
    9-15 July 2016)

2015

  1. 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
  2. Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Tonetta, Stefano,
    in «LOGICAL METHODS IN COMPUTER SCIENCE»,
    vol. 11,
    n. 4,
    2015
  3. Bozzano M.; Cimatti A.; Gario M.; Micheli A.,
    SMT-based 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)
  4. Bozzano, Marco; Cimatti, Alessandro; Griggio, Alberto; Mattarei, Cristian,
    Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I,
    vol.9206,
    2015
    , pp. 603-
    621
    , (27th International Conference on Computer Aided Verification, CAV 2015,
    San Francisco, CA,
    July 18-24, 2015)
  5. 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 18-24, 2015, Proceedings, Part I,
    vol.9206,
    2015
    , pp. 518-
    535
    , (27th International Conference on Computer Aided Verification (CAV),
    San Francisco, CA, USA,
    July 18-24, 2015)

2014

  1. 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
  2. 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,
    Springer-Verlag,
    vol.8413,
    2014
    , pp. 326-
    340
    , (Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014,
    Grenoble, Francia,
    2014)
  3. M. Bozzano; A. Cimatti; C. Mattarei; S. Tonetta,
    Formal Safety Assessment via Contract-Based Design.,
    ATVA14,
    2014
    , pp. 81-
    97
    , (Automated Technology for Verification and Analysis,
    Sydney,
  4. Bittner B.; Bozzano M.; Cimatti A.; Gario M.; Griggio A.,
    Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions,
    Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design,
    2014
    , pp. 23-
    30
  5. 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 SP-725,
    2014
    , (DASIA 2014,
    Warsaw, Poland,
    June 3rd - June 5th)
  6. 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. 82-
    95
    , (International Symposium on Model Based Safety and Assessment,
    Munich, Germany,
    October 27-29, 2014)
  7. Bittner B.; Bozzano M. ; Cimatti A.; De Ferluc R.; Gario M.; Guiotto A.; Yushtein Y.,
    FAME: A Model-Based Environment for FDIR Design in Aerospace,
    Proceedings of the International Symposium on Model Based Safety and Assessment,
    Springer International Publishing,
    vol.8822,
    2014
    , pp. 1-
    2
    , (International Symposium on Model Based Safety and Assessment,
    Munich, Germany,
    October 27-29, 2014)

2013

  1. 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
  2. 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
  3. Marco Bozzano; Adolfo Villafiorita,
    in Encyclopedia of Software Engineering,
    New York,
    CRC Press, Taylor & Francis Group,
    2013
  4. 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 17-19, 2013,
    IEEE Computer Society,
    2013
    , pp. 198-
    207
    , (International Conference on Engineering of Complex Computer Systems,
    Singapore,
    07/17/2013 07/19/2013)
  5. Bozzano M.; Cimatti A.; Gario M.; Tonetta S.,
    AAAI Workshops,
    2013
    , (Workshops at the Twenty-Seventh AAAI Conference on Artificial Intelligence,
    Bellevue, Washington, USA,
    14–18 July 2013)
  6. 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 1-4, 2013)
  7. 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. 279-
    294
    , (Ninth Haifa Verification Conference,
    Haiva, Israel,
    5 - 7 November 2013)

2012

  1. Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive,
    Symbolic Synthesis of Observability Requirements for Diagnosability,
    Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
    AAAI Press,
    2012
    , (AAAI 2012: Twenty-Sixth AAAI Conference on Artificial Intelligence,
    Toronto, Canada,
    da 07/22/2012 a 07/26/2012)
  2. 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

  1. Marco Bozzano; Alessandro Cimatti; Joost-Pieter 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
  2. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    A Comprehensive Approach to On-Board Autonomy Verification and Validation,
    AAAI (Conference on Artificial Intelligence)
    Press
    ,
    2011
    , (IJCAI 2011,
    Barcelona, Catalonia (Spain),
    16-22/07/2011)
  3. 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)
  4. 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

  1. Marco Bozzano; Adolfo Villafiorita,
    Design and Safety Assessment of Critical Systems,
    London,
    Auerbach Publications (Taylor & Francis Group),
    2010
  2. Marco Bozzano; Alessandro Cimatti; Joost-Pieter 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. 562-
    565
    , (CAV 2010,
    Edinburgh, UK,
    15-19/07/2010)
  3. Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Joost-Pieter 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,
    19-21/05/2010)
  4. 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/08-03/09/2010)
  5. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer; Roberto Cavada,
    2010,

2009

  1. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    Workshop on Verification and Validation of Planning and Scheduling Systems,
    2009
    , pp. 1-
    10
    , (VV&PS 2009 - ICAPS,
    Thessaloniki, Greece,
    20/09/2009)
  2. Marco Bozzano; Alessandro Cimatti; Joost-Pieter 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. 173-
    186
    , (SAFECOMP 2009,
    Hamburg, Germany,
    15-18/09/2009)
  3. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter 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. 285-
    286
    , (ESEC/FSE 2009,
    Amsterdam, The Netherlands,
    24-28/08/2009)
  4. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Proceedings 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems,
    CEUR-WS.org,
    vol.507,
    2009
    , pp. 87-
    91
    , (ACESMB09,
    Denver, Colorado, USA,
    06/10/2009)
  5. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll,
    Codesign of Dependable Systems: A Component-Based Modeling Language,
    Proceedings of the 7th IEEE/ACM Int. Conference on Formal Methods and Models for Codesign,
    Piscataway, NJ,
    2009
    , pp. 121-
    130
    , (MEMOCODE'09,
    Cambridge, Massachusetts, USA,
    13-15/07/2009)
  6. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Codesign of Dependable Systems: A Component-Based Language,
    2009
  7. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,
    2009

2008

  1. Marco Bozzano; Alessandro Cimatti; Andrea Guiotto; Andrea Martelli; Marco Roveri; Andrei Tchaltsev; Yuri Yushtein,
    On-Board 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)
  2. Alessandro Cimatti; Marco Bozzano; Adolfo Villafiorita,
    2008,

2007

  1. Marco Bozzano; Adolfo Villafiorita,
    The FSAP/NuSMV-SA Safety Analysis Platform,
    in «INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER»,
    vol. 9,
    n. 1,
    2007
    , pp. 5 -
    24
  2. Piergiorgio Bertoli; Marco Bozzano; Alessandro Cimatti,
    A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis,
    Model Checking and Artificial Intelligence,
    Berlin, Heidelberg,
    Springer-Verlag,
    2007
    , pp. 1 -
    18
  3. Marco Bozzano; Alessandro Cimatti; Francesco Tapparo,
    Symbolic Fault Tree Analysis for Reactive Systems,
    5th Int. Symposium on Automated Technology for Verification and Analysis,
    Springer-Verlag,
    vol.4762,
    2007
    , pp. 162-
    176
    , (ATVA 2007,
    Tokyo, Japan,
    22-25/10/2007)

2006

  1. 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
  2. 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. 3-
    14
    , (PDPAR 2005 affiliated workshop to CAV'05,
    University of Edinburgh, Scotland, UK,
    12/07/2005)
  3. 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. 127-
    141
    , (SAFECOMP 2006,
    Gdansk, Poland,
    26-29/09/2006)
  4. 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,
    25-27/01/2006)

2005

  1. 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. 1-3,
    2005
    , pp. 265 -
    293
  2. 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. 317-
    333
    , (TACAS 2005,
    Edinburgh, UK,
    04/04/2005 - 08/04/2005)
  3. 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. 315-
    321
    , (CADE-20,
    Tallin, Estonia,
    22-27/07/2005)
  4. 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. 17-
    32
    , (BMC 2004,
    Boston, MA, USA,
    18/07/2004)
  5. 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. 335-
    349
    , (CAV,
    University of Edinburgh, Scotland, UK,
    6-10/07/2005)
  6. 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. Nelson-Oppen, 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 non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art 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 non-convex 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 speed-ups up to two orders of magnitude
    ,
    2005
  7. 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 real-world problems (e.g. model-checking, circuit testing, propositional planning) by encoding into SAT.
    However, a purely boolean representation is not expressive enough for many other real-world 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, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art 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 theory-driven backjumping and learning, and theory-driven 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 stack-based 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 state-of-the-art 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
  8. 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 quantifier-free 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 real-world 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 Nelson-Oppen, 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 non-convex theories.
    We show the effectiveness of the approach by a thorough experimental comparison
    ,
    2005

2004

  1. M. Bozzano; G. Delzanno; M. Martelli,
    Model Checking Linear Logic Specifications,
    in «THEORY AND PRACTICE OF LOGIC PROGRAMMING»,
    vol. 4,
    n. 5-6,
    2004
    , pp. 573 -
    619
  2. 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
  3. 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)
  4. 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 new-generation 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
  5. 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 new-generation 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 word-level verification
    ,
    2004

2003

  1. 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)
  2. 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)
  3. Marco Bozzano; Adolfo Villafiorita,
    Improving System Reliability via Model Checking: the FSAP/NuSMV-SA Safety Analysis Platform,
    Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,
    2003
    , pp. 49-
    62
    , (Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,
    2003)
  4. 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. 208-
    222
    , (FME 2003: Formal Methods. Proceedings of the International Symposium of Formal Methods,
    2003)
  5. Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,
    CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    2003
    , pp. 62-
    76
    , (CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    Miami, USA,
    2003)
  6. Marco Bozzano; Adolfo Villafiorita,
    Improving System Reliability via Mdel Checking: the FSAP/NuSMV-SA 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/NuSMV-SA 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/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic 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 European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development,
    2003
  7. 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 European-Union-sponsored 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

  1. 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
  2. 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
  3. 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. 221-
    235
    , (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)
  4. Bozzano, Marco; Delzanno, Giorgio,
    Algorithmic Verification of Invalidation-Based Protocols,
    Computer Aided Verification,
    Heidelberg,
    Spinger,
    vol.2404,
    2002
    , pp. 295-
    308
    , (14th International Conference, CAV 2002,
    Copenhagen, Denmark,
    July 27–31, 2002)