UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Elizabeth Polgreen; Kevin Cheang; Pranav Gaddamadugu; Adwait Godbole; Kevin Laeufer; Shaokai Lin; Yatin A. Manerkar; Federico Mora; Sanjit A. Seshia

doi:10.1007/978-3-031-13185-1_27

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.

Original language	English
Title of host publication	Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I
Editors	Sharon Shoham, Yakir Vizel
Publisher	Springer, Cham
Pages	538–551
Number of pages	13
ISBN (Electronic)	978-3-031-13185-1
ISBN (Print)	978-3-031-13184-4
DOIs	https://doi.org/10.1007/978-3-031-13185-1_27
Publication status	Published - 7 Aug 2022
Event	34th International Conference on Computer-Aided Verification - Haifa, Israel Duration: 7 Aug 2022 → 10 Aug 2022 Conference number: 34 http://i-cav.org/2022/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Cham
Volume	13371
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	34th International Conference on Computer-Aided Verification
Abbreviated title	CAV 2022
Country/Territory	Israel
City	Haifa
Period	7/08/22 → 10/08/22
Internet address	http://i-cav.org/2022/

Access to Document

10.1007/978-3-031-13185-1_27Licence: Creative Commons: Attribution (CC-BY)

UCLID5_POLGREEN_DOA03062022_VOR_CC-BYFinal published version, 732 KBLicence: Creative Commons: Attribution (CC-BY)

https://link.springer.com/chapter/10.1007/978-3-031-13185-1_27Licence: Creative Commons: Attribution (CC-BY)

Cite this

Polgreen, E., Cheang, K., Gaddamadugu, P., Godbole, A., Laeufer, K., Lin, S., Manerkar, Y. A., Mora, F., & Seshia, S. A. (2022). UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. In S. Shoham, & Y. Vizel (Eds.), Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I (pp. 538–551). (Lecture Notes in Computer Science; Vol. 13371). Springer, Cham. https://doi.org/10.1007/978-3-031-13185-1_27

Polgreen, Elizabeth ; Cheang, Kevin ; Gaddamadugu, Pranav et al. / UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I. editor / Sharon Shoham ; Yakir Vizel. Springer, Cham, 2022. pp. 538–551 (Lecture Notes in Computer Science).

@inproceedings{2028f43b9e12434699742981ca1ffaa1,

title = "UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis",

abstract = "UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.",

author = "Elizabeth Polgreen and Kevin Cheang and Pranav Gaddamadugu and Adwait Godbole and Kevin Laeufer and Shaokai Lin and Manerkar, {Yatin A.} and Federico Mora and Seshia, {Sanjit A.}",

note = "Funding Information: Acknowledgments. The UCLID5 project is grateful for the significant contributions by Pramod Subramanyan, one of the original creators of the tool. This work was supported in part by NSF grant 1837132, the DARPA grant FA8750-20-C-0156 (LOGiCS), by the Qualcomm Innovation Fellowship, and by Amazon and Intel. Publisher Copyright: {\textcopyright} 2022, The Author(s).; 34th International Conference on Computer-Aided Verification, CAV 2022 ; Conference date: 07-08-2022 Through 10-08-2022",

year = "2022",

month = aug,

day = "7",

doi = "10.1007/978-3-031-13185-1_27",

language = "English",

isbn = "978-3-031-13184-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "538–551",

editor = "Shoham, {Sharon } and Vizel, {Yakir }",

booktitle = "Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I",

url = "http://i-cav.org/2022/",

}

Polgreen, E, Cheang, K, Gaddamadugu, P, Godbole, A, Laeufer, K, Lin, S, Manerkar, YA, Mora, F & Seshia, SA 2022, UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. in S Shoham & Y Vizel (eds), Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, Springer, Cham, pp. 538–551, 34th International Conference on Computer-Aided Verification, Haifa, Israel, 7/08/22. https://doi.org/10.1007/978-3-031-13185-1_27

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. / Polgreen, Elizabeth; Cheang, Kevin; Gaddamadugu, Pranav et al.

Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I. ed. / Sharon Shoham; Yakir Vizel. Springer, Cham, 2022. p. 538–551 (Lecture Notes in Computer Science; Vol. 13371).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

AU - Polgreen, Elizabeth

AU - Cheang, Kevin

AU - Gaddamadugu, Pranav

AU - Godbole, Adwait

AU - Laeufer, Kevin

AU - Lin, Shaokai

AU - Manerkar, Yatin A.

AU - Mora, Federico

AU - Seshia, Sanjit A.

N1 - Conference code: 34

PY - 2022/8/7

Y1 - 2022/8/7

N2 - UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.

AB - UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.

U2 - 10.1007/978-3-031-13185-1_27

DO - 10.1007/978-3-031-13185-1_27

M3 - Conference contribution

SN - 978-3-031-13184-4

T3 - Lecture Notes in Computer Science

SP - 538

EP - 551

BT - Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I

A2 - Shoham, Sharon

A2 - Vizel, Yakir

PB - Springer, Cham

T2 - 34th International Conference on Computer-Aided Verification

Y2 - 7 August 2022 through 10 August 2022

ER -

Polgreen E, Cheang K, Gaddamadugu P, Godbole A, Laeufer K, Lin S et al. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. In Shoham S, Vizel Y, editors, Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part I. Springer, Cham. 2022. p. 538–551. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-13185-1_27

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this