Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Alberto Griggio
@inproceedings{DBLP:conf/tacas/KonigHGKCHTKFH24,
author = {Lukas K{\"{o}}nig and
Christian Heinzemann and
Alberto Griggio and
Michaela Klauck and
Alessandro Cimatti and
Franziska Henze and
Stefano Tonetta and
Stefan K{\"{u}}perkoch and
Dennis Fassbender and
Michael Hanselmann},
editor = {Bernd Finkbeiner and
Laura Kov{\'{a}}cs},
title = {Towards Safe Autonomous Driving: Model Checking a Behavior Planner
during Development},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 30th International Conference, {TACAS} 2024, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings,
Part {II}},
series = {Lecture Notes in Computer Science},
volume = {14571},
pages = {44--65},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-57249-4\_3},
doi = {10.1007/978-3-031-57249-4\_3},
timestamp = {Sun, 14 Apr 2024 18:32:16 +0200},
biburl = {https://dblp.org/rec/conf/tacas/KonigHGKCHTKFH24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2402-19028,
author = {Gianluca Redondi and
Alessandro Cimatti and
Alberto Griggio and
Kenneth McMillan},
title = {Invariant Checking for SMT-based Systems with Quantifiers},
journal = {CoRR},
volume = {abs/2402.19028},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2402.19028},
doi = {10.48550/ARXIV.2402.19028},
eprinttype = {arXiv},
eprint = {2402.19028},
timestamp = {Tue, 26 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2402-19028.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2403-00087,
author = {Alessandro Cimatti and
Alberto Griggio and
Gianluca Redondi},
title = {Towards the verification of a generic interlocking logic: Dafny meets
parameterized model checking},
journal = {CoRR},
volume = {abs/2403.00087},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2403.00087},
doi = {10.48550/ARXIV.2403.00087},
eprinttype = {arXiv},
eprint = {2403.00087},
timestamp = {Tue, 02 Apr 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2403-00087.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/XiaBCGLP23,
author = {Yechuan Xia and
Anna Becchi and
Alessandro Cimatti and
Alberto Griggio and
Jianwen Li and
Geguang Pu},
editor = {Constantin Enea and
Akash Lal},
title = {Searching for i-Good Lemmas to Accelerate Safety Model Checking},
booktitle = {Computer Aided Verification - 35th International Conference, {CAV}
2023, Paris, France, July 17-22, 2023, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {13965},
pages = {288--308},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-37703-7\_14},
doi = {10.1007/978-3-031-37703-7\_14},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cav/XiaBCGLP23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/GriggioJ23,
author = {Alberto Griggio and
Martin Jon{\'{a}}s},
editor = {Constantin Enea and
Akash Lal},
title = {Kratos2: An SMT-Based Model Checker for Imperative Programs},
booktitle = {Computer Aided Verification - 35th International Conference, {CAV}
2023, Paris, France, July 17-22, 2023, Proceedings, Part {III}},
series = {Lecture Notes in Computer Science},
volume = {13966},
pages = {423--436},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-37709-9\_20},
doi = {10.1007/978-3-031-37709-9\_20},
timestamp = {Tue, 12 Sep 2023 07:57:21 +0200},
biburl = {https://dblp.org/rec/conf/cav/GriggioJ23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiCGTCNB23,
author = {Alessandro Cimatti and
Luca Cristoforetti and
Alberto Griggio and
Stefano Tonetta and
Sara Corfini and
Marco Di Natale and
Florian Barrau},
editor = {Sriram Sankaranarayanan and
Natasha Sharygina},
title = {{EVA:} a Tool for the Compositional Verification of {AUTOSAR} Models},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 29th International Conference, {TACAS} 2023, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {13994},
pages = {3--10},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-30820-8\_1},
doi = {10.1007/978-3-031-30820-8\_1},
timestamp = {Sat, 13 May 2023 01:07:18 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiCGTCNB23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2311-09784,
author = {Srajan Goyal and
Alberto Griggio and
Jacob Kimblad and
Stefano Tonetta},
editor = {Marie Farrell and
Matt Luckcuck and
Mario Gleirscher and
Maike Schwammberger},
title = {Automatic Generation of Scenarios for System-level Simulation-based
Verification of Autonomous Driving Systems},
booktitle = {Proceedings Fifth International Workshop on Formal Methods for Autonomous
Systems, FMAS@iFM 2023, Leiden, The Netherlands, 15th and 16th of
November 2023},
series = {{EPTCS}},
volume = {395},
pages = {113--129},
year = {2023},
url = {https://doi.org/10.4204/EPTCS.395.8},
doi = {10.4204/EPTCS.395.8},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2311-09784.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/CimattiGMRT22,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Marco Roveri and
Stefano Tonetta},
title = {Verification modulo theories},
journal = {Formal Methods Syst. Des.},
volume = {60},
number = {3},
pages = {452--481},
year = {2022},
url = {https://doi.org/10.1007/s10703-023-00434-x},
doi = {10.1007/S10703-023-00434-X},
timestamp = {Wed, 01 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/CimattiGMRT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/CimattiGM22,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Magnago},
title = {{LTL} falsification in infinite-state systems},
journal = {Inf. Comput.},
volume = {289},
number = {Part},
pages = {104977},
year = {2022},
url = {https://doi.org/10.1016/j.ic.2022.104977},
doi = {10.1016/J.IC.2022.104977},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/CimattiGM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/MannIGPB22,
author = {Makai Mann and
Ahmed Irfan and
Alberto Griggio and
Oded Padon and
Clark W. Barrett},
title = {Counterexample-Guided Prophecy for Model Checking Modulo the Theory
of Arrays},
journal = {Log. Methods Comput. Sci.},
volume = {18},
number = {3},
year = {2022},
url = {https://doi.org/10.46298/lmcs-18(3:26)2022},
doi = {10.46298/LMCS-18(3:26)2022},
timestamp = {Sun, 16 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/MannIGPB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/atva/CimattiGLS22,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Lipparini and
Roberto Sebastiani},
editor = {Ahmed Bouajjani and
Luk{\'{a}}s Hol{\'{\i}}k and
Zhilin Wu},
title = {Handling Polynomial and Transcendental Functions in {SMT} via Unconstrained
Optimisation and Topological Degree Test},
booktitle = {Automated Technology for Verification and Analysis - 20th International
Symposium, {ATVA} 2022, Virtual Event, October 25-28, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13505},
pages = {137--153},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-19992-9\_9},
doi = {10.1007/978-3-031-19992-9\_9},
timestamp = {Sun, 06 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/atva/CimattiGLS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/atva/CimattiGR22,
author = {Alessandro Cimatti and
Alberto Griggio and
Gianluca Redondi},
editor = {Ahmed Bouajjani and
Luk{\'{a}}s Hol{\'{\i}}k and
Zhilin Wu},
title = {Verification of {SMT} Systems with Quantifiers},
booktitle = {Automated Technology for Verification and Analysis - 20th International
Symposium, {ATVA} 2022, Virtual Event, October 25-28, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13505},
pages = {154--170},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-19992-9\_10},
doi = {10.1007/978-3-031-19992-9\_10},
timestamp = {Sun, 13 Nov 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/atva/CimattiGR22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/imbsa/BombardelliBCCG22,
author = {Alberto Bombardelli and
Marco Bozzano and
Roberto Cavada and
Alessandro Cimatti and
Alberto Griggio and
Massimo Nazaria and
Edoardo Nicolodi and
Stefano Tonetta},
editor = {Christel Seguin and
Marc Zeller and
Tatiana Prosvirnova},
title = {{COMPASTA:} Extending {TASTE} with Formal Design and Verification
Functionality},
booktitle = {Model-Based Safety and Assessment - 8th International Symposium, {IMBSA}
2022, Munich, Germany, September 5-7, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13525},
pages = {21--27},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-15842-1\_2},
doi = {10.1007/978-3-031-15842-1\_2},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/imbsa/BombardelliBCCG22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpnmr/BozzanoCGJK22,
author = {Marco Bozzano and
Alessandro Cimatti and
Alberto Griggio and
Martin Jon{\'{a}}s and
Greg Kimberly},
editor = {Georg Gottlob and
Daniela Inclezan and
Marco Maratea},
title = {Analysis of Cyclic Fault Propagation via {ASP}},
booktitle = {Logic Programming and Nonmonotonic Reasoning - 16th International
Conference, {LPNMR} 2022, Genova, Italy, September 5-9, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13416},
pages = {470--483},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-15707-3\_36},
doi = {10.1007/978-3-031-15707-3\_36},
timestamp = {Thu, 22 Sep 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpnmr/BozzanoCGJK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/models/CimattiCCNGPT22,
author = {Alessandro Cimatti and
Sara Corfini and
Luca Cristoforetti and
Marco Di Natale and
Alberto Griggio and
Stefano Puri and
Stefano Tonetta},
editor = {Eugene Syriani and
Houari A. Sahraoui and
Nelly Bencomo and
Manuel Wimmer},
title = {A comprehensive framework for the analysis of automotive systems},
booktitle = {Proceedings of the 25th International Conference on Model Driven Engineering
Languages and Systems, {MODELS} 2022, Montreal, Quebec, Canada, October
23-28, 2022},
pages = {379--389},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3550355.3552408},
doi = {10.1145/3550355.3552408},
timestamp = {Thu, 27 Oct 2022 15:55:50 +0200},
biburl = {https://dblp.org/rec/conf/models/CimattiCCNGPT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sefm/CavadaCGS22,
author = {Roberto Cavada and
Alessandro Cimatti and
Alberto Griggio and
Angelo Susi},
editor = {Paolo Masci and
Cinzia Bernardeschi and
Pierluigi Graziani and
Mario Koddenbrock and
Maurizio Palmieri},
title = {A Formal {IDE} for Railways: Research Challenges},
booktitle = {Software Engineering and Formal Methods. {SEFM} 2022 Collocated Workshops
- AI4EA, F-IDE, CoSim-CPS, CIFMA, Berlin, Germany, September 26-30,
2022, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {13765},
pages = {107--115},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-26236-4\_9},
doi = {10.1007/978-3-031-26236-4\_9},
timestamp = {Tue, 28 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sefm/CavadaCGS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/CimattiGT22,
author = {Alessandro Cimatti and
Alberto Griggio and
Stefano Tonetta},
editor = {David D{\'{e}}harbe and
Antti E. J. Hyv{\"{a}}rinen},
title = {The {VMT-LIB} Language and Tools},
booktitle = {Proceedings of the 20th Internal Workshop on Satisfiability Modulo
Theories co-located with the 11th International Joint Conference on
Automated Reasoning {(IJCAR} 2022) part of the 8th Federated Logic
Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3185},
pages = {80--89},
publisher = {CEUR-WS.org},
year = {2022},
url = {https://ceur-ws.org/Vol-3185/extended9547.pdf},
timestamp = {Fri, 10 Mar 2023 16:22:48 +0100},
biburl = {https://dblp.org/rec/conf/smt/CimattiGT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BozzanoCGJ22,
author = {Marco Bozzano and
Alessandro Cimatti and
Alberto Griggio and
Martin Jon{\'{a}}s},
editor = {Dana Fisman and
Grigore Rosu},
title = {Efficient Analysis of Cyclic Redundancy Architectures via Boolean
Fault Propagation},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 28th International Conference, {TACAS} 2022, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {13244},
pages = {273--291},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-030-99527-0\_15},
doi = {10.1007/978-3-030-99527-0\_15},
timestamp = {Fri, 29 Apr 2022 14:50:32 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BozzanoCGJ22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2022,
editor = {Alberto Griggio and
Neha Rungta},
title = {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022, Trento,
Italy, October 17-21, 2022},
publisher = {{IEEE}},
year = {2022},
url = {https://ieeexplore.ieee.org/xpl/conhome/10026543/proceeding},
isbn = {978-3-85448-053-2},
timestamp = {Mon, 13 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/fmcad/2022.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/AbrahamDEG22,
author = {Erika {\'{A}}brah{\'{a}}m and
James H. Davenport and
Matthew England and
Alberto Griggio},
title = {New Perspectives in Symbolic Computation and Satisfiability Checking
(Dagstuhl Seminar 22072)},
journal = {Dagstuhl Reports},
volume = {12},
number = {2},
pages = {67--86},
year = {2022},
url = {https://doi.org/10.4230/DagRep.12.2.67},
doi = {10.4230/DAGREP.12.2.67},
timestamp = {Mon, 26 Sep 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/dagstuhl-reports/AbrahamDEG22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/GriggioRT21,
author = {Alberto Griggio and
Marco Roveri and
Stefano Tonetta},
title = {Certifying proofs for SAT-based model checking},
journal = {Formal Methods Syst. Des.},
volume = {57},
number = {2},
pages = {178--210},
year = {2021},
url = {https://doi.org/10.1007/s10703-021-00369-1},
doi = {10.1007/S10703-021-00369-1},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fmsd/GriggioRT21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/atva/CimattiGM21,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Magnago},
editor = {Zhe Hou and
Vijay Ganesh},
title = {Automatic Discovery of Fair Paths in Infinite-State Transition Systems},
booktitle = {Automated Technology for Verification and Analysis - 19th International
Symposium, {ATVA} 2021, Gold Coast, QLD, Australia, October 18-22,
2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12971},
pages = {32--47},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-88885-5\_3},
doi = {10.1007/978-3-030-88885-5\_3},
timestamp = {Wed, 03 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/atva/CimattiGM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/CimattiGR21,
author = {Alessandro Cimatti and
Alberto Griggio and
Gianluca Redondi},
editor = {Andr{\'{e}} Platzer and
Geoff Sutcliffe},
title = {Universal Invariant Checking of Parametric Systems with Quantifier-free
{SMT} Reasoning},
booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12699},
pages = {131--147},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-79876-5\_8},
doi = {10.1007/978-3-030-79876-5\_8},
timestamp = {Thu, 29 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/CimattiGR21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BozzanoCPGJK20,
author = {Marco Bozzano and
Alessandro Cimatti and
Anthony Fernandes Pires and
Alberto Griggio and
Martin Jon{\'{a}}s and
Greg Kimberly},
editor = {Alexandra Silva and
K. Rustan M. Leino},
title = {Efficient SMT-Based Analysis of Failure Propagation},
booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
2021, Virtual Event, July 20-23, 2021, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12760},
pages = {209--230},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-81688-9\_10},
doi = {10.1007/978-3-030-81688-9\_10},
timestamp = {Thu, 12 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/BozzanoCPGJK20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/MoverCGIT21,
author = {Sergio Mover and
Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Stefano Tonetta},
editor = {Alexandra Silva and
K. Rustan M. Leino},
title = {Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems},
booktitle = {Computer Aided Verification - 33rd International Conference, {CAV}
2021, Virtual Event, July 20-23, 2021, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12759},
pages = {529--551},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-81685-8\_25},
doi = {10.1007/978-3-030-81685-8\_25},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/MoverCGIT21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BigarellaCGIJRS21,
author = {Filippo Bigarella and
Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Martin Jon{\'{a}}s and
Marco Roveri and
Roberto Sebastiani and
Patrick Trentin},
editor = {Boris Konev and
Giles Reger},
title = {Optimization Modulo Non-linear Arithmetic via Incremental Linearization},
booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS
2021, Birmingham, UK, September 8-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12941},
pages = {213--231},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-86205-3\_12},
doi = {10.1007/978-3-030-86205-3\_12},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/frocos/BigarellaCGIJRS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/MannIGPB21,
author = {Makai Mann and
Ahmed Irfan and
Alberto Griggio and
Oded Padon and
Clark W. Barrett},
editor = {Jan Friso Groote and
Kim Guldstrand Larsen},
title = {Counterexample-Guided Prophecy for Model Checking Modulo the Theory
of Arrays},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 27th International Conference, {TACAS} 2021, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings,
Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12651},
pages = {113--132},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-72016-2\_7},
doi = {10.1007/978-3-030-72016-2\_7},
timestamp = {Fri, 14 May 2021 08:34:19 +0200},
biburl = {https://dblp.org/rec/conf/tacas/MannIGPB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/CimattiGM21,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Magnago},
editor = {Fritz Henglein and
Sharon Shoham and
Yakir Vizel},
title = {Proving the Existence of Fair Paths in Infinite-State Systems},
booktitle = {Verification, Model Checking, and Abstract Interpretation - 22nd International
Conference, {VMCAI} 2021, Copenhagen, Denmark, January 17-19, 2021,
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12597},
pages = {104--126},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-67067-2\_6},
doi = {10.1007/978-3-030-67067-2\_6},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/vmcai/CimattiGM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2101-06825,
author = {Makai Mann and
Ahmed Irfan and
Alberto Griggio and
Oded Padon and
Clark W. Barrett},
title = {Counterexample-Guided Prophecy for Model Checking Modulo the Theory
of Arrays},
journal = {CoRR},
volume = {abs/2101.06825},
year = {2021},
url = {https://arxiv.org/abs/2101.06825},
eprinttype = {arXiv},
eprint = {2101.06825},
timestamp = {Fri, 22 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2101-06825.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2109-12821,
author = {Alessandro Cimatti and
Alberto Griggio and
Stefano Tonetta},
title = {The {VMT-LIB} Language and Tools},
journal = {CoRR},
volume = {abs/2109.12821},
year = {2021},
url = {https://arxiv.org/abs/2109.12821},
eprinttype = {arXiv},
eprint = {2109.12821},
timestamp = {Mon, 04 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2109-12821.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/CimattiGMRT20,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Magnago and
Marco Roveri and
Stefano Tonetta},
title = {SMT-based satisfiability of first-order {LTL} with event freezing
functions and metric operators},
journal = {Inf. Comput.},
volume = {272},
pages = {104502},
year = {2020},
url = {https://doi.org/10.1016/j.ic.2019.104502},
doi = {10.1016/J.IC.2019.104502},
timestamp = {Fri, 14 May 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iandc/CimattiGMRT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsc/DavenportEGST20,
author = {James H. Davenport and
Matthew England and
Alberto Griggio and
Thomas Sturm and
Cesare Tinelli},
title = {Symbolic computation and satisfiability checking},
journal = {J. Symb. Comput.},
volume = {100},
pages = {1--10},
year = {2020},
url = {https://doi.org/10.1016/j.jsc.2019.07.017},
doi = {10.1016/J.JSC.2019.07.017},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsc/DavenportEGST20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/isola/AmendolaBCCGSST20,
author = {Arturo Amendola and
Anna Becchi and
Roberto Cavada and
Alessandro Cimatti and
Alberto Griggio and
Giuseppe Scaglione and
Angelo Susi and
Alberto Tacchella and
Matteo Tessi},
editor = {Tiziana Margaria and
Bernhard Steffen},
title = {A Model-Based Approach to the Design, Verification and Deployment
of Railway Interlocking System},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation:
Applications - 9th International Symposium on Leveraging Applications
of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020,
Proceedings, Part {III}},
series = {Lecture Notes in Computer Science},
volume = {12478},
pages = {240--254},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-61467-6\_16},
doi = {10.1007/978-3-030-61467-6\_16},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/isola/AmendolaBCCGSST20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGGKT20,
author = {Alessandro Cimatti and
Luca Geatti and
Alberto Griggio and
Greg Kimberly and
Stefano Tonetta},
editor = {Armin Biere and
David Parker},
title = {Safe Decomposition of Startup Requirements: Verification and Synthesis},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 26th International Conference, {TACAS} 2020, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12078},
pages = {155--172},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-45190-5\_9},
doi = {10.1007/978-3-030-45190-5\_9},
timestamp = {Fri, 14 May 2021 08:34:17 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGGKT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CimattiGMRT19,
author = {Alessandro Cimatti and
Alberto Griggio and
Enrico Magnago and
Marco Roveri and
Stefano Tonetta},
editor = {Isil Dillig and
Serdar Tasiran},
title = {Extending nuXmv with Timed Transition Systems and Timed Temporal Properties},
booktitle = {Computer Aided Verification - 31st International Conference, {CAV}
2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part
{I}},
series = {Lecture Notes in Computer Science},
volume = {11561},
pages = {376--386},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-25540-4\_21},
doi = {10.1007/978-3-030-25540-4\_21},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/CimattiGMRT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpsweek/FrehseAABBCGGMM19,
author = {Goran Frehse and
Alessandro Abate and
Dieky Adzkiya and
Anna Becchi and
Lei Bu and
Alessandro Cimatti and
Mirco Giacobbe and
Alberto Griggio and
Sergio Mover and
Muhammad Syifa'ul Mufid and
Idriss Riouak and
Stefano Tonetta and
Enea Zaffanella},
editor = {Goran Frehse and
Matthias Althoff},
title = {{ARCH-COMP19} Category Report: Hybrid Systems with Piecewise Constant
Dynamics},
booktitle = {{ARCH19.} 6th International Workshop on Applied Verification of Continuous
and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada,
April 15, 2019},
series = {EPiC Series in Computing},
volume = {61},
pages = {1--13},
publisher = {EasyChair},
year = {2019},
url = {https://doi.org/10.29007/rjwn},
doi = {10.29007/RJWN},
timestamp = {Wed, 07 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpsweek/FrehseAABBCGGMM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/scsquare/IrfanCGRS19,
author = {Ahmed Irfan and
Alessandro Cimatti and
Alberto Griggio and
Marco Roveri and
Roberto Sebastiani},
editor = {John Abbott and
Alberto Griggio},
title = {Lemmas for Satisfiability Modulo Transcendental Functions via Incremental
Linearization},
booktitle = {Proceedings of the 4th SC-Square Workshop co-located with the {SIAM}
Conference on Applied Algebraic Geometry, SC-square@SIAM {AG} 2019,
Bern, Switzerland, 10th July 2019},
series = {{CEUR} Workshop Proceedings},
volume = {2460},
publisher = {CEUR-WS.org},
year = {2019},
url = {http://ceur-ws.org/Vol-2460/paper8.pdf},
timestamp = {Mon, 28 Aug 2023 17:23:07 +0200},
biburl = {https://dblp.org/rec/conf/scsquare/IrfanCGRS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/scsquare/2019,
editor = {John Abbott and
Alberto Griggio},
title = {Proceedings of the 4th SC-Square Workshop co-located with the {SIAM}
Conference on Applied Algebraic Geometry, SC-square@SIAM {AG} 2019,
Bern, Switzerland, 10th July 2019},
series = {{CEUR} Workshop Proceedings},
volume = {2460},
publisher = {CEUR-WS.org},
year = {2019},
url = {http://ceur-ws.org/Vol-2460},
urn = {urn:nbn:de:0074-2460-6},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/scsquare/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/CimattiGIRS18,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
title = {Incremental Linearization for Satisfiability and Verification Modulo
Nonlinear Arithmetic and Transcendental Functions},
journal = {{ACM} Trans. Comput. Log.},
volume = {19},
number = {3},
pages = {19:1--19:52},
year = {2018},
url = {https://doi.org/10.1145/3230639},
doi = {10.1145/3230639},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tocl/CimattiGIRS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/GriggioRT18,
author = {Alberto Griggio and
Marco Roveri and
Stefano Tonetta},
editor = {Nikolaj S. Bj{\o}rner and
Arie Gurfinkel},
title = {Certifying Proofs for {LTL} Model Checking},
booktitle = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin,
TX, USA, October 30 - November 2, 2018},
pages = {1--9},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.23919/FMCAD.2018.8603022},
doi = {10.23919/FMCAD.2018.8603022},
timestamp = {Thu, 14 Apr 2022 20:26:15 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/GriggioRT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/CimattiGIRS18,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
editor = {Olaf Beyersdorff and
Christoph M. Wintersteiger},
title = {Experimenting on Solving Nonlinear Integer Arithmetic with Incremental
Linearization},
booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2018 - 21st
International Conference, {SAT} 2018, Held as Part of the Federated
Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10929},
pages = {383--398},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94144-8\_23},
doi = {10.1007/978-3-319-94144-8\_23},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sat/CimattiGIRS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sigsoft/MechtaevGCR18,
author = {Sergey Mechtaev and
Alberto Griggio and
Alessandro Cimatti and
Abhik Roychoudhury},
editor = {Gary T. Leavens and
Alessandro Garcia and
Corina S. Pasareanu},
title = {Symbolic execution with existential second-order constraints},
booktitle = {Proceedings of the 2018 {ACM} Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering,
{ESEC/SIGSOFT} {FSE} 2018, Lake Buena Vista, FL, USA, November 04-09,
2018},
pages = {389--399},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3236024.3236049},
doi = {10.1145/3236024.3236049},
timestamp = {Tue, 01 Feb 2022 10:45:16 +0100},
biburl = {https://dblp.org/rec/conf/sigsoft/MechtaevGCR18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/CimattiGIRS18,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
title = {Incremental linearization: {A} practical approach to satisfiability
modulo nonlinear arithmetic and transcendental functions},
booktitle = {20th International Symposium on Symbolic and Numeric Algorithms for
Scientific Computing, {SYNASC} 2018, Timisoara, Romania, September
20-23, 2018},
pages = {19--26},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.1109/SYNASC.2018.00016},
doi = {10.1109/SYNASC.2018.00016},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/synasc/CimattiGIRS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1801-08718,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
title = {Invariant Checking of {NRA} Transition Systems via Incremental Reduction
to {LRA} with {EUF}},
journal = {CoRR},
volume = {abs/1801.08718},
year = {2018},
url = {http://arxiv.org/abs/1801.08718},
eprinttype = {arXiv},
eprint = {1801.08718},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1801-08718.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1801-08723,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
title = {Satisfiability Modulo Transcendental Functions via Incremental Linearization},
journal = {CoRR},
volume = {abs/1801.08723},
year = {2018},
url = {http://arxiv.org/abs/1801.08723},
eprinttype = {arXiv},
eprint = {1801.08723},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1801-08723.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/GriggioR17,
author = {Alberto Griggio and
Philipp R{\"{u}}mmer},
title = {Preface to special issue on satisfiability modulo theories},
journal = {Formal Methods Syst. Des.},
volume = {51},
number = {3},
pages = {431--432},
year = {2017},
url = {https://doi.org/10.1007/s10703-017-0308-5},
doi = {10.1007/S10703-017-0308-5},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fmsd/GriggioR17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/AbrahamA0BBCDEF17,
author = {Erika {\'{A}}brah{\'{a}}m and
John Abbott and
Bernd Becker and
Anna Maria Bigatti and
Martin Brain and
Alessandro Cimatti and
James H. Davenport and
Matthew England and
Pascal Fontaine and
Stephen Forrest and
Vijay Ganesh and
Alberto Griggio and
Daniel Kroening and
Werner M. Seiler},
editor = {Giles Reger and
Dmitriy Traytel},
title = {SC-square: when Satisfiability Checking and Symbolic Computation join
forces},
booktitle = {{ARCADE} 2017, 1st International Workshop on Automated Reasoning:
Challenges, Applications, Directions, Exemplary Achievements, Gothenburg,
Sweden, 6th August 2017},
series = {EPiC Series in Computing},
volume = {51},
pages = {6--10},
publisher = {EasyChair},
year = {2017},
url = {https://doi.org/10.29007/p319},
doi = {10.29007/P319},
timestamp = {Mon, 31 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/AbrahamA0BBCDEF17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/CimattiGIRS17,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
editor = {Leonardo de Moura},
title = {Satisfiability Modulo Transcendental Functions via Incremental Linearization},
booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10395},
pages = {95--113},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63046-5\_7},
doi = {10.1007/978-3-319-63046-5\_7},
timestamp = {Thu, 29 Sep 2022 08:36:56 +0200},
biburl = {https://dblp.org/rec/conf/cade/CimattiGIRS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/issac/BrainDG17,
author = {Martin Brain and
James H. Davenport and
Alberto Griggio},
editor = {Matthew England and
Vijay Ganesh},
title = {Benchmarking Solvers, SAT-style},
booktitle = {Proceedings of the 2nd International Workshop on Satisfiability Checking
and Symbolic Computation co-located with the 42nd International Symposium
on Symbolic and Algebraic Computation {(ISSAC} 2017), Kaiserslautern,
Germany, July 29, 2017},
series = {{CEUR} Workshop Proceedings},
volume = {1974},
publisher = {CEUR-WS.org},
year = {2017},
url = {https://ceur-ws.org/Vol-1974/RP3.pdf},
timestamp = {Fri, 10 Mar 2023 16:22:18 +0100},
biburl = {https://dblp.org/rec/conf/issac/BrainDG17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGIRS17,
author = {Alessandro Cimatti and
Alberto Griggio and
Ahmed Irfan and
Marco Roveri and
Roberto Sebastiani},
editor = {Axel Legay and
Tiziana Margaria},
title = {Invariant Checking of {NRA} Transition Systems via Incremental Reduction
to {LRA} with {EUF}},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference, {TACAS} 2017, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {10205},
pages = {58--75},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54577-5\_4},
doi = {10.1007/978-3-662-54577-5\_4},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGIRS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cca/AbrahamA0BBBCDE16,
author = {Erika {\'{A}}brah{\'{a}}m and
John Abbott and
Bernd Becker and
Anna Maria Bigatti and
Martin Brain and
Bruno Buchberger and
Alessandro Cimatti and
James H. Davenport and
Matthew England and
Pascal Fontaine and
Stephen Forrest and
Alberto Griggio and
Daniel Kroening and
Werner M. Seiler and
Thomas Sturm},
title = {Satisfiability checking and symbolic computation},
journal = {{ACM} Commun. Comput. Algebra},
volume = {50},
number = {4},
pages = {145--147},
year = {2016},
url = {https://doi.org/10.1145/3055282.3055285},
doi = {10.1145/3055282.3055285},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/cca/AbrahamA0BBBCDE16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/CimattiGMT16,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
title = {Infinite-state invariant checking with {IC3} and predicate abstraction},
journal = {Formal Methods Syst. Des.},
volume = {49},
number = {3},
pages = {190--218},
year = {2016},
url = {https://doi.org/10.1007/s10703-016-0257-4},
doi = {10.1007/S10703-016-0257-4},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fmsd/CimattiGMT16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcad/GriggioR16,
author = {Alberto Griggio and
Marco Roveri},
title = {Comparing Different Variants of the ic3 Algorithm for Hardware Model
Checking},
journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
volume = {35},
number = {6},
pages = {1026--1039},
year = {2016},
url = {https://doi.org/10.1109/TCAD.2015.2481869},
doi = {10.1109/TCAD.2015.2481869},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tcad/GriggioR16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/DanielCGTM16,
author = {Jakub Daniel and
Alessandro Cimatti and
Alberto Griggio and
Stefano Tonetta and
Sergio Mover},
editor = {Swarat Chaudhuri and
Azadeh Farzan},
title = {Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded
Relations},
booktitle = {Computer Aided Verification - 28th International Conference, {CAV}
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {9779},
pages = {271--291},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-41528-4\_15},
doi = {10.1007/978-3-319-41528-4\_15},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/DanielCGTM16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/date/IrfanCGRS16,
author = {Ahmed Irfan and
Alessandro Cimatti and
Alberto Griggio and
Marco Roveri and
Roberto Sebastiani},
editor = {Luca Fanucci and
J{\"{u}}rgen Teich},
title = {Verilog2SMV: {A} tool for word-level verification},
booktitle = {2016 Design, Automation {\&} Test in Europe Conference {\&}
Exhibition, {DATE} 2016, Dresden, Germany, March 14-18, 2016},
pages = {1156--1159},
publisher = {{IEEE}},
year = {2016},
url = {https://ieeexplore.ieee.org/document/7459485/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/date/IrfanCGRS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/AbrahamABBBBCDE16,
author = {Erika {\'{A}}brah{\'{a}}m and
John Abbott and
Bernd Becker and
Anna Maria Bigatti and
Martin Brain and
Bruno Buchberger and
Alessandro Cimatti and
James H. Davenport and
Matthew England and
Pascal Fontaine and
Stephen Forrest and
Alberto Griggio and
Daniel Kroening and
Werner M. Seiler and
Thomas Sturm},
editor = {Michael Kohlhase and
Moa Johansson and
Bruce R. Miller and
Leonardo de Moura and
Frank Wm. Tompa},
title = {SC\({}^{\mbox{2}}\): Satisfiability Checking Meets Symbolic Computation
- (Project Paper)},
booktitle = {Intelligent Computer Mathematics - 9th International Conference, {CICM}
2016, Bialystok, Poland, July 25-29, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9791},
pages = {28--43},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-42547-4\_3},
doi = {10.1007/978-3-319-42547-4\_3},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/mkm/AbrahamABBBBCDE16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BittnerBCCGGMMZ16,
author = {Benjamin Bittner and
Marco Bozzano and
Roberto Cavada and
Alessandro Cimatti and
Marco Gario and
Alberto Griggio and
Cristian Mattarei and
Andrea Micheli and
Gianni Zampedri},
editor = {Marsha Chechik and
Jean{-}Fran{\c{c}}ois Raskin},
title = {The xSAP Safety Analysis Platform},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 22nd International Conference, {TACAS} 2016, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9636},
pages = {533--539},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-662-49674-9\_31},
doi = {10.1007/978-3-662-49674-9\_31},
timestamp = {Sun, 25 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BittnerBCCGGMMZ16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/AbrahamABBBBCDE16,
author = {Erika {\'{A}}brah{\'{a}}m and
John Abbott and
Bernd Becker and
Anna Maria Bigatti and
Martin Brain and
Bruno Buchberger and
Alessandro Cimatti and
James H. Davenport and
Matthew England and
Pascal Fontaine and
Stephen Forrest and
Alberto Griggio and
Daniel Kroening and
Werner M. Seiler and
Thomas Sturm},
title = {Satisfiability Checking and Symbolic Computation},
journal = {CoRR},
volume = {abs/1607.06945},
year = {2016},
url = {http://arxiv.org/abs/1607.06945},
eprinttype = {arXiv},
eprint = {1607.06945},
timestamp = {Mon, 31 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/AbrahamABBBBCDE16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/AbrahamABBBBCDE16a,
author = {Erika {\'{A}}brah{\'{a}}m and
John Abbott and
Bernd Becker and
Anna Maria Bigatti and
Martin Brain and
Bruno Buchberger and
Alessandro Cimatti and
James H. Davenport and
Matthew England and
Pascal Fontaine and
Stephen Forrest and
Alberto Griggio and
Daniel Kroening and
Werner M. Seiler and
Thomas Sturm},
title = {Satisfiability Checking meets Symbolic Computation (Project Paper)},
journal = {CoRR},
volume = {abs/1607.08028},
year = {2016},
url = {http://arxiv.org/abs/1607.08028},
eprinttype = {arXiv},
eprint = {1607.08028},
timestamp = {Mon, 31 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/AbrahamABBBBCDE16a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BozzanoCGM15,
author = {Marco Bozzano and
Alessandro Cimatti and
Alberto Griggio and
Cristian Mattarei},
editor = {Daniel Kroening and
Corina S. Pasareanu},
title = {Efficient Anytime Techniques for Model-Based Safety Analysis},
booktitle = {Computer Aided Verification - 27th International Conference, {CAV}
2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part
{I}},
series = {Lecture Notes in Computer Science},
volume = {9206},
pages = {603--621},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21690-4\_41},
doi = {10.1007/978-3-319-21690-4\_41},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/BozzanoCGM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/syncop/CimattiGMT15,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
editor = {{\'{E}}tienne Andr{\'{e}} and
Goran Frehse},
title = {Parameter Synthesis with {IC3} (Informal Presentation)},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters, SynCoP
2015, April 11, 2015, London, United Kingdom},
series = {OASIcs},
volume = {44},
pages = {106--107},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2015},
url = {https://doi.org/10.4230/OASIcs.SynCoP.2015.106},
doi = {10.4230/OASICS.SYNCOP.2015.106},
timestamp = {Tue, 15 Feb 2022 09:40:05 +0100},
biburl = {https://dblp.org/rec/conf/syncop/CimattiGMT15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGMT15,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
editor = {Christel Baier and
Cesare Tinelli},
title = {HyComp: An SMT-Based Model Checker for Hybrid Systems},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 21st International Conference, {TACAS} 2015, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2015, London, UK, April 11-18, 2015. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9035},
pages = {52--67},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-46681-0\_4},
doi = {10.1007/978-3-662-46681-0\_4},
timestamp = {Sat, 30 Sep 2023 09:57:43 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGMT15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BittnerBCCGGMMZ15,
author = {Benjamin Bittner and
Marco Bozzano and
Roberto Cavada and
Alessandro Cimatti and
Marco Gario and
Alberto Griggio and
Cristian Mattarei and
Andrea Micheli and
Gianni Zampedri},
title = {The xSAP Safety Analysis Platform},
journal = {CoRR},
volume = {abs/1504.07513},
year = {2015},
url = {http://arxiv.org/abs/1504.07513},
eprinttype = {arXiv},
eprint = {1504.07513},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BittnerBCCGGMMZ15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/BrainDGHK14,
author = {Martin Brain and
Vijay Victor D'Silva and
Alberto Griggio and
Leopold Haller and
Daniel Kroening},
title = {Deciding floating-point logic with abstract conflict driven clause
learning},
journal = {Formal Methods Syst. Des.},
volume = {45},
number = {2},
pages = {213--245},
year = {2014},
url = {https://doi.org/10.1007/s10703-013-0203-7},
doi = {10.1007/S10703-013-0203-7},
timestamp = {Tue, 16 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/fmsd/BrainDGHK14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CavadaCDGMMMRT14,
author = {Roberto Cavada and
Alessandro Cimatti and
Michele Dorigatti and
Alberto Griggio and
Alessandro Mariotti and
Andrea Micheli and
Sergio Mover and
Marco Roveri and
Stefano Tonetta},
editor = {Armin Biere and
Roderick Bloem},
title = {The nuXmv Symbolic Model Checker},
booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 18-22, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {334--342},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08867-9\_22},
doi = {10.1007/978-3-319-08867-9\_22},
timestamp = {Mon, 03 Jan 2022 22:13:44 +0100},
biburl = {https://dblp.org/rec/conf/cav/CavadaCDGMMMRT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CimattiGMT14,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
editor = {Armin Biere and
Roderick Bloem},
title = {Verifying {LTL} Properties of Hybrid Systems with K-Liveness},
booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 18-22, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {424--440},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08867-9\_28},
doi = {10.1007/978-3-319-08867-9\_28},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/CimattiGMT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/BittnerBCGG14,
author = {Benjamin Bittner and
Marco Bozzano and
Alessandro Cimatti and
Marco Gario and
Alberto Griggio},
title = {Towards Pareto-optimal parameter synthesis for monotonic cost functions},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland,
October 21-24, 2014},
pages = {23--30},
publisher = {{IEEE}},
year = {2014},
url = {https://doi.org/10.1109/FMCAD.2014.6987591},
doi = {10.1109/FMCAD.2014.6987591},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/BittnerBCGG14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGMT14,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
editor = {Erika {\'{A}}brah{\'{a}}m and
Klaus Havelund},
title = {{IC3} Modulo Theories via Implicit Predicate Abstraction},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 20th International Conference, {TACAS} 2014, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2014, Grenoble, France, April 5-13, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8413},
pages = {46--61},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-642-54862-8\_4},
doi = {10.1007/978-3-642-54862-8\_4},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGMT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/CimattiGS14,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
title = {Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories},
journal = {CoRR},
volume = {abs/1401.3878},
year = {2014},
url = {http://arxiv.org/abs/1401.3878},
eprinttype = {arXiv},
eprint = {1401.3878},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/CimattiGS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/CimattiGMT13,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
title = {Parameter synthesis with {IC3}},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2013, Portland, OR,
USA, October 20-23, 2013},
pages = {165--168},
publisher = {{IEEE}},
year = {2013},
url = {https://ieeexplore.ieee.org/document/6679406/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/CimattiGMT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/BrainDGHK13,
author = {Martin Brain and
Vijay Victor D'Silva and
Alberto Griggio and
Leopold Haller and
Daniel Kroening},
editor = {Francesco Logozzo and
Manuel F{\"{a}}hndrich},
title = {Interpolation-Based Verification of Floating-Point Programs with Abstract
{CDCL}},
booktitle = {Static Analysis - 20th International Symposium, {SAS} 2013, Seattle,
WA, USA, June 20-22, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7935},
pages = {412--432},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-38856-9\_22},
doi = {10.1007/978-3-642-38856-9\_22},
timestamp = {Tue, 16 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sas/BrainDGHK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/CimattiGSS13,
author = {Alessandro Cimatti and
Alberto Griggio and
Bastiaan Joost Schaafsma and
Roberto Sebastiani},
editor = {Matti J{\"{a}}rvisalo and
Allen Van Gelder},
title = {A Modular Approach to MaxSAT Modulo Theories},
booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2013 - 16th
International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7962},
pages = {150--165},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39071-5\_12},
doi = {10.1007/978-3-642-39071-5\_12},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sat/CimattiGSS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGSS13,
author = {Alessandro Cimatti and
Alberto Griggio and
Bastiaan Joost Schaafsma and
Roberto Sebastiani},
editor = {Nir Piterman and
Scott A. Smolka},
title = {The MathSAT5 {SMT} Solver},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 19th International Conference, {TACAS} 2013, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2013, Rome, Italy, March 16-24, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7795},
pages = {93--107},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-36742-7\_7},
doi = {10.1007/978-3-642-36742-7\_7},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGSS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/BrainDHGK13,
author = {Martin Brain and
Vijay Victor D'Silva and
Leopold Haller and
Alberto Griggio and
Daniel Kroening},
editor = {Roberto Giacobazzi and
Josh Berdine and
Isabella Mastroeni},
title = {An Abstract Interpretation of {DPLL(T)}},
booktitle = {Verification, Model Checking, and Abstract Interpretation, 14th International
Conference, {VMCAI} 2013, Rome, Italy, January 20-22, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7737},
pages = {455--475},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-35873-9\_27},
doi = {10.1007/978-3-642-35873-9\_27},
timestamp = {Tue, 16 Nov 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/vmcai/BrainDHGK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/CimattiGMT13,
author = {Alessandro Cimatti and
Alberto Griggio and
Sergio Mover and
Stefano Tonetta},
title = {{IC3} Modulo Theories via Implicit Predicate Abstraction},
journal = {CoRR},
volume = {abs/1310.6847},
year = {2013},
url = {http://arxiv.org/abs/1310.6847},
eprinttype = {arXiv},
eprint = {1310.6847},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/CimattiGMT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsat/Griggio12,
author = {Alberto Griggio},
title = {A Practical Approach to Satisability Modulo Linear Integer Arithmetic},
journal = {J. Satisf. Boolean Model. Comput.},
volume = {8},
number = {1/2},
pages = {1--27},
year = {2012},
url = {https://doi.org/10.3233/sat190086},
doi = {10.3233/SAT190086},
timestamp = {Mon, 17 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsat/Griggio12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BruttomessoG12,
author = {Roberto Bruttomesso and
Alberto Griggio},
editor = {Vladimir Klebanov and
Bernhard Beckert and
Armin Biere and
Geoff Sutcliffe},
title = {Broadening the Scope of {SMT-COMP:} the Application Track},
booktitle = {Proceedings of the 1st International Workshop on Comparative Empirical
Evaluation of Reasoning Systems, Manchester, United Kingdom, June
30, 2012},
series = {{CEUR} Workshop Proceedings},
volume = {873},
pages = {18--27},
publisher = {CEUR-WS.org},
year = {2012},
url = {https://ceur-ws.org/Vol-873/papers/paper\_7.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:14 +0100},
biburl = {https://dblp.org/rec/conf/cade/BruttomessoG12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/CokGBD12,
author = {David R. Cok and
Alberto Griggio and
Roberto Bruttomesso and
Morgan Deters},
editor = {Pascal Fontaine and
Amit Goel},
title = {The 2012 {SMT} Competition},
booktitle = {10th International Workshop on Satisfiability Modulo Theories, {SMT}
2012, Manchester, UK, June 30 - July 1, 2012},
series = {EPiC Series in Computing},
volume = {20},
pages = {131--142},
publisher = {EasyChair},
year = {2012},
url = {https://doi.org/10.29007/gj66},
doi = {10.29007/GJ66},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/CokGBD12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/caise/AliGFDG12,
author = {Raian Ali and
Alberto Griggio and
Anders Franz{\'{e}}n and
Fabiano Dalpiaz and
Paolo Giorgini},
editor = {Ilia Bider and
Terry A. Halpin and
John Krogstie and
Selmin Nurcan and
Erik Proper and
Rainer Schmidt and
Pnina Soffer and
Stanislaw Wrycza},
title = {Optimizing Monitoring Requirements in Self-adaptive Systems},
booktitle = {Enterprise, Business-Process and Information Systems Modeling - 13th
International Conference, {BPMDS} 2012, 17th International Conference,
{EMMSAD} 2012, and 5th EuroSymposium, held at CAiSE 2012, Gda{\'{n}}sk,
Poland, June 25-26, 2012. Proceedings},
series = {Lecture Notes in Business Information Processing},
volume = {113},
pages = {362--377},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31072-0\_25},
doi = {10.1007/978-3-642-31072-0\_25},
timestamp = {Sun, 25 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/caise/AliGFDG12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CimattiG12,
author = {Alessandro Cimatti and
Alberto Griggio},
editor = {P. Madhusudan and
Sanjit A. Seshia},
title = {Software Model Checking via {IC3}},
booktitle = {Computer Aided Verification - 24th International Conference, {CAV}
2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7358},
pages = {277--293},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31424-7\_23},
doi = {10.1007/978-3-642-31424-7\_23},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/CimattiG12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/HallerGBK12,
author = {Leopold Haller and
Alberto Griggio and
Martin Brain and
Daniel Kroening},
editor = {Gianpiero Cabodi and
Satnam Singh},
title = {Deciding floating-point logic with systematic abstraction},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge,
UK, October 22-25, 2012},
pages = {131--140},
publisher = {{IEEE}},
year = {2012},
url = {https://ieeexplore.ieee.org/document/6462565/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/HallerGBK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jair/CimattiGS11,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
title = {Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories},
journal = {J. Artif. Intell. Res.},
volume = {40},
pages = {701--728},
year = {2011},
url = {https://doi.org/10.1613/jair.3196},
doi = {10.1613/JAIR.3196},
timestamp = {Sat, 21 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jair/CimattiGS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/CimattiGMNR11,
author = {Alessandro Cimatti and
Alberto Griggio and
Andrea Micheli and
Iman Narasamdya and
Marco Roveri},
editor = {Ganesh Gopalakrishnan and
Shaz Qadeer},
title = {Kratos - {A} Software Model Checker for SystemC},
booktitle = {Computer Aided Verification - 23rd International Conference, {CAV}
2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6806},
pages = {310--316},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22110-1\_24},
doi = {10.1007/978-3-642-22110-1\_24},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/CimattiGMNR11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/Griggio11,
author = {Alberto Griggio},
editor = {Per Bjesse and
Anna Slobodov{\'{a}}},
title = {Effective word-level interpolation for software verification},
booktitle = {International Conference on Formal Methods in Computer-Aided Design,
{FMCAD} '11, Austin, TX, USA, October 30 - November 02, 2011},
pages = {28--36},
publisher = {{FMCAD} Inc.},
year = {2011},
url = {http://dl.acm.org/citation.cfm?id=2157662},
timestamp = {Mon, 09 Aug 2021 15:21:44 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/Griggio11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/GriggioPST11,
author = {Alberto Griggio and
Quoc{-}Sang Phan and
Roberto Sebastiani and
Silvia Tomasi},
editor = {Cesare Tinelli and
Viorica Sofronie{-}Stokkermans},
title = {Stochastic Local Search for {SMT:} Combining Theory Solvers with WalkSAT},
booktitle = {Frontiers of Combining Systems, 8th International Symposium, FroCoS
2011, Saarbr{\"{u}}cken, Germany, October 5-7, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6989},
pages = {163--178},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-24364-6\_12},
doi = {10.1007/978-3-642-24364-6\_12},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/frocos/GriggioPST11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/GriggioLS11,
author = {Alberto Griggio and
Thi Thieu Hoa Le and
Roberto Sebastiani},
editor = {Parosh Aziz Abdulla and
K. Rustan M. Leino},
title = {Efficient Interpolant Generation in Satisfiability Modulo Linear Integer
Arithmetic},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 17th International Conference, {TACAS} 2011, Held as Part of the
Joint European Conferences on Theory and Practice of Software, {ETAPS}
2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6605},
pages = {143--157},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-19835-9\_13},
doi = {10.1007/978-3-642-19835-9\_13},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/GriggioLS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1010-4422,
author = {Alberto Griggio and
Thi Thieu Hoa Le and
Roberto Sebastiani},
title = {Efficient Interpolant Generation in Satisfiability Modulo Linear Integer
Arithmetic},
journal = {Log. Methods Comput. Sci.},
volume = {8},
number = {3},
year = {2010},
url = {https://doi.org/10.2168/LMCS-8(3:3)2012},
doi = {10.2168/LMCS-8(3:3)2012},
timestamp = {Sun, 16 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1010-4422.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/CimattiGS10,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
title = {Efficient generation of craig interpolants in satisfiability modulo
theories},
journal = {{ACM} Trans. Comput. Log.},
volume = {12},
number = {1},
pages = {7:1--7:54},
year = {2010},
url = {https://doi.org/10.1145/1838552.1838559},
doi = {10.1145/1838552.1838559},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tocl/CimattiGS10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/date/CimattiFGKR10,
author = {Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Krishnamani Kalyanasundaram and
Marco Roveri},
editor = {Giovanni De Micheli and
Bashir M. Al{-}Hashimi and
Wolfgang M{\"{u}}ller and
Enrico Macii},
title = {Tighter integration of BDDs and {SMT} for Predicate Abstraction},
booktitle = {Design, Automation and Test in Europe, {DATE} 2010, Dresden, Germany,
March 8-12, 2010},
pages = {1707--1712},
publisher = {{IEEE} Computer Society},
year = {2010},
url = {https://doi.org/10.1109/DATE.2010.5457090},
doi = {10.1109/DATE.2010.5457090},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/date/CimattiFGKR10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiFGSS10,
author = {Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Roberto Sebastiani and
Cristian Stenico},
editor = {Javier Esparza and
Rupak Majumdar},
title = {Satisfiability Modulo the Theory of Costs: Foundations and Applications},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
16th International Conference, {TACAS} 2010, Held as Part of the Joint
European Conferences on Theory and Practice of Software, {ETAPS} 2010,
Paphos, Cyprus, March 20-28, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6015},
pages = {99--113},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-12002-2\_8},
doi = {10.1007/978-3-642-12002-2\_8},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiFGSS10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/basesearch/Griggio09,
author = {Alberto Griggio},
title = {An Effective {SMT} Engine for Formal Verification},
school = {University of Trento, Italy},
year = {2009},
url = {http://eprints-phd.biblio.unitn.it/166/},
timestamp = {Thu, 27 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/basesearch/Griggio09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/amai/BruttomessoCFGS09,
author = {Roberto Bruttomesso and
Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Roberto Sebastiani},
title = {Delayed theory combination vs. Nelson-Oppen for satisfiability modulo
theories: a comparative analysis},
journal = {Ann. Math. Artif. Intell.},
volume = {55},
number = {1-2},
pages = {63--99},
year = {2009},
url = {https://doi.org/10.1007/s10472-009-9152-7},
doi = {10.1007/S10472-009-9152-7},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/amai/BruttomessoCFGS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/CimattiGS09,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
editor = {Renate A. Schmidt},
title = {Interpolant Generation for {UTVPI}},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5663},
pages = {167--182},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02959-2\_15},
doi = {10.1007/978-3-642-02959-2\_15},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/CimattiGS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/BeyerCGKS09,
author = {Dirk Beyer and
Alessandro Cimatti and
Alberto Griggio and
M. Erkan Keremoglu and
Roberto Sebastiani},
title = {Software model checking via large-block encoding},
booktitle = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided
Design, {FMCAD} 2009, 15-18 November 2009, Austin, Texas, {USA}},
pages = {25--32},
publisher = {{IEEE}},
year = {2009},
url = {https://doi.org/10.1109/FMCAD.2009.5351147},
doi = {10.1109/FMCAD.2009.5351147},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/BeyerCGKS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0904-4709,
author = {Dirk Beyer and
Alessandro Cimatti and
Alberto Griggio and
M. Erkan Keremoglu and
Roberto Sebastiani},
title = {Software Model Checking via Large-Block Encoding},
journal = {CoRR},
volume = {abs/0904.4709},
year = {2009},
url = {http://arxiv.org/abs/0904.4709},
eprinttype = {arXiv},
eprint = {0904.4709},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0904-4709.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0906-4492,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
title = {Efficient Generation of Craig Interpolants in Satisfiability Modulo
Theories},
journal = {CoRR},
volume = {abs/0906.4492},
year = {2009},
url = {http://arxiv.org/abs/0906.4492},
eprinttype = {arXiv},
eprint = {0906.4492},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0906-4492.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BruttomessoCFGS08,
author = {Roberto Bruttomesso and
Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Roberto Sebastiani},
editor = {Aarti Gupta and
Sharad Malik},
title = {The MathSAT 4SMT Solver},
booktitle = {Computer Aided Verification, 20th International Conference, {CAV}
2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5123},
pages = {299--303},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-70545-1\_28},
doi = {10.1007/978-3-540-70545-1\_28},
timestamp = {Sat, 30 Sep 2023 09:35:55 +0200},
biburl = {https://dblp.org/rec/conf/cav/BruttomessoCFGS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/CimattiGS08,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
editor = {C. R. Ramakrishnan and
Jakob Rehof},
title = {Efficient Interpolant Generation in Satisfiability Modulo Theories},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
14th International Conference, {TACAS} 2008, Held as Part of the Joint
European Conferences on Theory and Practice of Software, {ETAPS} 2008,
Budapest, Hungary, March 29-April 6, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4963},
pages = {397--412},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-78800-3\_30},
doi = {10.1007/978-3-540-78800-3\_30},
timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
biburl = {https://dblp.org/rec/conf/tacas/CimattiGS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BruttomessoCFGHNPS07,
author = {Roberto Bruttomesso and
Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Ziyad Hanna and
Alexander Nadel and
Amit Palti and
Roberto Sebastiani},
editor = {Werner Damm and
Holger Hermanns},
title = {A Lazy and Layered SMT({\textdollar}{\textbackslash}mathcal\{BV\}{\textdollar})
Solver for Hard Industrial Verification Problems},
booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
2007, Berlin, Germany, July 3-7, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4590},
pages = {547--560},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73368-3\_54},
doi = {10.1007/978-3-540-73368-3\_54},
timestamp = {Sat, 30 Sep 2023 09:35:55 +0200},
biburl = {https://dblp.org/rec/conf/cav/BruttomessoCFGHNPS07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/CimattiGS07,
author = {Alessandro Cimatti and
Alberto Griggio and
Roberto Sebastiani},
editor = {Jo{\~{a}}o Marques{-}Silva and
Karem A. Sakallah},
title = {A Simple and Flexible Way of Computing Small Unsatisfiable Cores in
{SAT} Modulo Theories},
booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2007, 10th
International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4501},
pages = {334--339},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-72788-0\_32},
doi = {10.1007/978-3-540-72788-0\_32},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sat/CimattiGS07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BruttomessoCFGS06,
author = {Roberto Bruttomesso and
Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Roberto Sebastiani},
editor = {Miki Hermann and
Andrei Voronkov},
title = {Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo
Theories: {A} Comparative Analysis},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
13-17, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4246},
pages = {527--541},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11916277\_36},
doi = {10.1007/11916277\_36},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BruttomessoCFGS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BruttomessoCFGSS06,
author = {Roberto Bruttomesso and
Alessandro Cimatti and
Anders Franz{\'{e}}n and
Alberto Griggio and
Alessandro Santuari and
Roberto Sebastiani},
editor = {Miki Hermann and
Andrei Voronkov},
title = {To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling
Uninterpreted Function Symbols in \emph{SMT}(\emph{EUF} {\`{E}}\emph{T})},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
13-17, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4246},
pages = {557--571},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11916277\_38},
doi = {10.1007/11916277\_38},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BruttomessoCFGSS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-04-15 23:28 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
