BibSLEIGH — Alessandro

Travelled to:

1 × Austria
1 × Cyprus
1 × Estonia
1 × Finland
1 × Hungary
1 × Israel
1 × New Zealand
1 × Poland
1 × Taiwan
2 × Canada
2 × Denmark
2 × Portugal
2 × South Africa
2 × The Netherlands
3 × France
3 × Germany
4 × United Kingdom
6 × Italy
8 × USA

Collaborated with:

M.Roveri A.Griggio S.Tonetta R.Sebastiani S.Mover M.Bozzano F.Giunchiglia E.M.Clarke R.Bruttomesso R.Bloem A.Franzén I.Narasamdya V.Schuppan I.Pill C.Mattarei P.Bertoli B.J.Schaafsma M.Benedetti A.Susi M.Gario A.Biere Y.Zhu M.Dorigatti T.A.Junttila P.v.Rossum A.Micheli R.Cavada A.Tchaltsev M.Pistore S.Semprini P.Traverso J.Katoen V.Y.Nguyen T.Noll S.Schulz S.Mechtaev A.Roychoudhury A.Mariotti K.Kalyanasundaram C.Stenico G.Audemard A.Kornilowicz M.Fujita P.L.Pieraccini A.Villafiorita J.Daniel K.Y.Rozier A.Irfan E.Magnago R.Wimmer S.Ranise A.F.Pires D.Jones G.Kimberly T.Petri R.Robinson R.Corvino A.Lazzaro T.Rizzo A.Sanseviero K.Greimel G.Hofferek R.Könighofer R.Seeber A.Chiappini L.Macchi O.Rebollo B.Vittorini Z.Hanna A.Nadel A.Palti E.Giunchiglia A.Tacchella P.Pecchiari B.Pietra J.Profeta D.Romano B.Yu M.Pensallorto

Talks about:

model (16) system (10) symbol (10) check (10) sat (9) theori (7) modulo (7) satisfi (6) formal (6) abstract (5)

Person: Alessandro Cimatti

DBLP: Cimatti:Alessandro

Facilitated 2 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2007

2006

2005

2003

2002

2001

1999

1997

1994

2018

2016

2017

2019

Wrote 56 papers:

CAV-2015-BozzanoCGM #analysis #modelling #performance #safety: Efficient Anytime Techniques for Model-Based Safety Analysis (MB, AC, AG, CM), pp. 603–621.
CAV-2015-BozzanoCPJKPRT #analysis #design #safety: Formal Design and Safety Analysis of AIR6110 Wheel Brake System (MB, AC, AFP, DJ, GK, TP, RR, ST), pp. 518–535.
TACAS-2015-CimattiGMT #hybrid #model checking #named #smt: HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.
CAV-2014-CavadaCDGMMMRT #model checking: The nuXmv Symbolic Model Checker (RC, AC, MD, AG, AM, AM, SM, MR, ST), pp. 334–342.
CAV-2014-CimattiGMT #hybrid #ltl #verification: Verifying LTL Properties of Hybrid Systems with K-Liveness (AC, AG, SM, ST), pp. 424–440.
TACAS-2014-BozzanoCGT #component #design #detection #fault #identification #logic #using: Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic (MB, AC, MG, ST), pp. 326–340.
TACAS-2014-CimattiGMT #abstraction #modulo theories: IC3 Modulo Theories via Implicit Predicate Abstraction (AC, AG, SM, ST), pp. 46–61.
ASE-2013-CimattiDT #contract #named #refinement: OCRA: A tool for checking the refinement of temporal contracts (AC, MD, ST), pp. 702–705.
SAT-2013-CimattiGSS #approach #composition #modulo theories #satisfiability: A Modular Approach to MaxSAT Modulo Theories (AC, AG, BJS, RS), pp. 150–165.
TACAS-2013-CimattiGSS #smt: The MathSAT5 SMT Solver (AC, AG, BJS, RS), pp. 93–107.
CAV-2012-CimattiCLNRRST #industrial #validation #verification: Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System (AC, RC, AL, IN, TR, MR, AS, AT), pp. 378–393.
CAV-2012-CimattiG #model checking: Software Model Checking via IC3 (AC, AG), pp. 277–293.
CAV-2011-CimattiGMNR #model checking #named: Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
CAV-2011-CimattiMT #automaton #hybrid #performance #verification: Efficient Scenario Verification for Hybrid Automata (AC, SM, ST), pp. 317–332.
TACAS-2011-CimattiNR #abstraction #lazy evaluation #partial order #reduction: Boosting Lazy Abstraction for SystemC with Partial Order Reduction (AC, IN, MR), pp. 341–356.
CAV-2010-BloemCGHKRSS #analysis #named #requirements #synthesis: RATSY — A New Requirements Analysis Tool with Synthesis (RB, AC, KG, GH, RK, MR, VS, RS), pp. 425–429.
CAV-2010-BozzanoCKNNRW #model checking: A Model Checker for AADL (MB, AC, JPK, VYN, TN, MR, RW), pp. 562–565.
CIAA-2010-CimattiMRT #automaton #nondeterminism #regular expression: From Sequential Extended Regular Expressions to NFA with Symbolic Labels (AC, SM, MR, ST), pp. 87–94.
DATE-2010-CimattiFGKR #abstraction #integration #smt: Tighter integration of BDDs and SMT for Predicate Abstraction (AC, AF, AG, KK, MR), pp. 1707–1712.
ICSE-2010-ChiappiniCMRRSTV #formal method #set #validation: Formalization and validation of a subset of the European Train Control System (AC, AC, LM, OR, MR, AS, ST, BV), pp. 109–118.
TACAS-2010-CimattiFGSS #formal method #satisfiability: Satisfiability Modulo the Theory of Costs: Foundations and Applications (AC, AF, AG, RS, CS), pp. 99–113.
ASE-2009-CavadaCMMMMPRST #requirements #validation: Supporting Requirements Validation: The EuRailCheck Tool (RC, AC, AM, CM, AM, SM, MP, MR, AS, ST), pp. 665–667.
CADE-2009-CimattiGS #generative: Interpolant Generation for UTVPI (AC, AG, RS), pp. 167–182.
CAV-2009-CimattiRT #hybrid #requirements #validation: Requirements Validation for Hybrid Systems (AC, MR, ST), pp. 188–203.
ESEC-FSE-2009-BozzanoCRKNN #evaluation #modelling #performance #verification: Verification and performance evaluation of aadl models (MB, AC, MR, JPK, VYN, TN), pp. 285–286.
CAV-2008-BruttomessoCFGS #smt: The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.
SEFM-2008-CimattiRST #constraints #modelling: Object Models with Temporal Constraints (AC, MR, AS, ST), pp. 249–258.
TACAS-2008-CimattiGS #generative #modulo theories #performance #satisfiability: Efficient Interpolant Generation in Satisfiability Modulo Theories (AC, AG, RS), pp. 397–412.
VMCAI-2008-CimattiRST: Diagnostic Information for Realizability (AC, MR, VS, AT), pp. 52–67.
CAV-2007-BruttomessoCFGHNPS #industrial #lazy evaluation #problem #smt #verification: A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems (RB, AC, AF, AG, ZH, AN, AP, RS), pp. 547–560.
CAV-2007-CimattiRST #abstraction #logic #satisfiability: Boolean Abstraction for Temporal Logic Satisfiability (AC, MR, VS, ST), pp. 532–546.
SAT-2007-CimattiGS #flexibility #modulo theories #satisfiability: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories (AC, AG, RS), pp. 334–339.
TACAS-2007-CimattiRT #optimisation #verification: Syntactic Optimizations for PSL Verification (AC, MR, ST), pp. 505–518.
CIAA-2006-BloemCPRS #automaton #implementation: Symbolic Implementation of Alternating Automata (RB, AC, IP, MR, SS), pp. 208–218.
CIAA-J-2006-BloemCPR07 #automaton #implementation: Symbolic Implementation of Alternating Automata (RB, AC, IP, MR), pp. 727–743.
DAC-2006-PillSCRBC #analysis #formal method #hardware #requirements: Formal analysis of hardware requirements (IP, SS, RC, MR, RB, AC), pp. 821–826.
SFM-2006-CimattiS #performance #satisfiability: Building Efficient Decision Procedures on Top of SAT Solvers (AC, RS), pp. 144–175.
CADE-2005-BozzanoBCJRSS: The MathSAT 3 System (MB, RB, AC, TAJ, PvR, SS, RS), pp. 315–321.
CAV-2005-BozzanoBCJRRS #modulo theories #performance #satisfiability: Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.
TACAS-2005-BozzanoBCJRSS #incremental #linear #logic #satisfiability: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.
TACAS-2003-BenedettiC #bound #ltl #model checking: Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
CADE-2002-AudemardBCKS #approach #linear #satisfiability: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (GA, PB, AC, AK, RS), pp. 195–210.
CAV-2002-CimattiCGGPRST #model checking: NuSMV 2: An OpenSource Tool for Symbolic Model Checking (AC, EMC, EG, FG, MP, MR, RS, AT), pp. 359–364.
VMCAI-2002-CimattiPRS #encoding #ltl #model checking #satisfiability: Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
TACAS-2001-CimattiRB #automaton #model checking #set: Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (AC, MR, PB), pp. 313–327.
CAV-1999-CimattiCGR #named #verification: NUSMV: A New Symbolic Model Verifier (AC, EMC, FG, MR), pp. 495–499.
DAC-1999-BiereCCFZ #model checking #satisfiability #using: Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
FM-v2-1999-CimattiPSTV #communication #protocol #specification #validation: Formal Specification and Validation of a Vital Communication Protocol (AC, PLP, RS, PT, AV), pp. 1584–1604.
TACAS-1999-BiereCCZ #model checking: Symbolic Model Checking without BDDs (AB, AC, EMC, YZ), pp. 193–207.
CAV-1997-CimattiGPPPRTY #certification #embedded #safety #verification: A Provably Correct Embedded Verifier for the Certification of Safety Critical Software (AC, FG, PP, BP, JP, DR, PT, BY), pp. 202–213.
LOPSTR-1994-GiunchigliaC #reasoning: Introspective Metatheoretic Reasoning (FG, AC), pp. 425–439.
ESEC-FSE-2018-MechtaevGCR #constraints #execution #higher-order #symbolic computation: Symbolic execution with existential second-order constraints (SM, AG, AC, AR), pp. 389–399.
CAV-2016-DanielCGTM #abstraction #infinity: Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations (JD, AC, AG, ST, SM), pp. 271–291.
CAV-2016-GarioCMTR #automation #design #model checking #scalability: Model Checking at Scale: Automated Air Traffic Control Design Space Exploration (MG, AC, CM, ST, KYR), pp. 3–22.
CADE-2017-CimattiGIRS #incremental #satisfiability: Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.
CAV-2019-CimattiGMRT: Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (AC, AG, EM, MR, ST), pp. 376–386.