Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929682414305280 |
|---|---|
| author | Cristiá, Maximiliano Rossi, Gianfranco |
| author_facet | Cristiá, Maximiliano Rossi, Gianfranco |
| contents | In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a Constraint Logic Programming (CLP) language and satisfiability solver based on set theory. Hence, we proceed as follows: a) a type system for {log} is defined; b) the constraint solver is proved to be safe w.r.t. the type system; c) the implementation of a concrete typechecker is presented; d) the integration of type checking and set constraint solving to increase automation during software verification is discussed; and f) two industrial-strength case studies are presented where this combination is used with very good results.
Under consideration in Theory and Practice of Logic Programming (TPLP) |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2205_01713 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification Cristiá, Maximiliano Rossi, Gianfranco Logic in Computer Science Programming Languages In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a Constraint Logic Programming (CLP) language and satisfiability solver based on set theory. Hence, we proceed as follows: a) a type system for {log} is defined; b) the constraint solver is proved to be safe w.r.t. the type system; c) the implementation of a concrete typechecker is presented; d) the integration of type checking and set constraint solving to increase automation during software verification is discussed; and f) two industrial-strength case studies are presented where this combination is used with very good results. Under consideration in Theory and Practice of Logic Programming (TPLP) |
| title | Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2205.01713 |