BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Cyprus
1 × Finland
1 × France
1 × Hungary
1 × Portugal
2 × Italy
2 × United Kingdom
3 × Germany
5 × USA
Collaborated with:
A.Cimatti R.Sebastiani S.Tonetta S.Mover M.Roveri A.Franzén R.Bruttomesso B.J.Schaafsma M.Brain V.D'Silva L.Haller D.Kröning T.T.H.Le A.Micheli M.Bozzano C.Mattarei D.R.Cok M.Deters S.Mechtaev A.Roychoudhury I.Narasamdya K.Kalyanasundaram C.Stenico J.Daniel A.Irfan E.Magnago Z.Hanna A.Nadel A.Palti R.Cavada M.Dorigatti A.Mariotti
Talks about:
modulo (7) smt (6) abstract (5) theori (5) model (5) interpol (4) satisfi (4) system (4) sat (4) generat (3)

Person: Alberto Griggio

DBLP DBLP: Griggio:Alberto

Contributed to:

CAV 20152015
TACAS 20152015
CAV 20142014
TACAS 20142014
SAS 20132013
SAT 20132013
TACAS 20132013
VMCAI 20132013
CAV 20122012
SMT 20122012
CAV 20112011
TACAS 20112011
DATE 20102010
TACAS 20102010
CADE 20092009
CAV 20082008
TACAS 20082008
CAV 20072007
SAT 20072007
ESEC/FSE 20182018
CAV (1) 20162016
CADE 20172017
CAV (1) 20192019

Wrote 24 papers:

CAV-2015-BozzanoCGM #analysis #modelling #performance #safety
Efficient Anytime Techniques for Model-Based Safety Analysis (MB, AC, AG, CM), pp. 603–621.
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-CimattiGMT #abstraction #modulo theories
IC3 Modulo Theories via Implicit Predicate Abstraction (AC, AG, SM, ST), pp. 46–61.
SAS-2013-BrainDGHK #float #source code #verification
Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL (MB, VD, AG, LH, DK), pp. 412–432.
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.
VMCAI-2013-BrainDHGK #abstract interpretation
An Abstract Interpretation of DPLL(T) (MB, VD, LH, AG, DK), pp. 455–475.
CAV-2012-CimattiG #model checking
Software Model Checking via IC3 (AC, AG), pp. 277–293.
SMT-2012-CokGBD #contest #smt
The 2012 SMT Competition (DRC, AG, RB, MD), pp. 131–142.
CAV-2011-CimattiGMNR #model checking #named
Kratos — A Software Model Checker for SystemC (AC, AG, AM, IN, MR), pp. 310–316.
TACAS-2011-GriggioLS #generative #integer #linear #performance #satisfiability
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic (AG, TTHL, RS), pp. 143–157.
DATE-2010-CimattiFGKR #abstraction #integration #smt
Tighter integration of BDDs and SMT for Predicate Abstraction (AC, AF, AG, KK, MR), pp. 1707–1712.
TACAS-2010-CimattiFGSS #formal method #satisfiability
Satisfiability Modulo the Theory of Costs: Foundations and Applications (AC, AF, AG, RS, CS), pp. 99–113.
CADE-2009-CimattiGS #generative
Interpolant Generation for UTVPI (AC, AG, RS), pp. 167–182.
CAV-2008-BruttomessoCFGS #smt
The MathSAT 4SMT Solver (RB, AC, AF, AG, RS), pp. 299–303.
TACAS-2008-CimattiGS #generative #modulo theories #performance #satisfiability
Efficient Interpolant Generation in Satisfiability Modulo Theories (AC, AG, RS), pp. 397–412.
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.
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.
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.
CADE-2017-CimattiGIRS #incremental #satisfiability
Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.
Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (AC, AG, EM, MR, ST), pp. 376–386.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.