HyperQB: A Bounded Model Checker for Hyperproperties
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2021
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917029552848896 |
|---|---|
| author | Hsu, Tzu-Han Rabizadeh, Milad Rogale, Kenneth Filippov, Fedor Batista, Marco A. de Oliveira Sánchez, César Bonakdarpour, Borzoo |
| author_facet | Hsu, Tzu-Han Rabizadeh, Milad Rogale, Kenneth Filippov, Fedor Batista, Marco A. de Oliveira Sánchez, César Bonakdarpour, Borzoo |
| contents | We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2109_12989 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | HyperQB: A Bounded Model Checker for Hyperproperties Hsu, Tzu-Han Rabizadeh, Milad Rogale, Kenneth Filippov, Fedor Batista, Marco A. de Oliveira Sánchez, César Bonakdarpour, Borzoo Logic in Computer Science Cryptography and Security We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools. |
| title | HyperQB: A Bounded Model Checker for Hyperproperties |
| topic | Logic in Computer Science Cryptography and Security |
| url | https://arxiv.org/abs/2109.12989 |