Document Search Results

Newest Citations Relevance

Zavalía, Lucas; Chernigovskaia, Lidiia; Fedyukovich, Grigory

Solving constrained Horn clauses over algebraic data types. (English) Zbl 1529.68167

Dragoi, Cezara (ed.) et al., Verification, model checking, and abstract interpretation. 24th international conference, VMCAI 2023, Boston, MA, USA, January 16–17, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13881, 341-365 (2023).

MSC: 68Q60 03B70 68Q65

Cite Review PDF

Full Text: DOI

Hetzl, Stefan; Vierling, Jannik

Induction and Skolemization in saturation theorem proving. (English) Zbl 07601550

Ann. Pure Appl. Logic 174, No. 1, Article ID 103167, 37 p. (2023).

MSC: 03F30 68V15 03B70 03H15

Cite Review PDF

Full Text: DOI arXiv

OA License

De Angelis, Emanuele; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio

Analysis and transformation of constrained Horn clauses for program verification. (English) Zbl 1541.68215

Theory Pract. Log. Program. 22, No. 6, 974-1042 (2022).

MSC: 68Q60 68N17 68N30

Cite Review PDF

Full Text: DOI arXiv

OA License

Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Reger, Giles; Voronkov, Andrei

Getting saturated with induction. (English) Zbl 1528.68391

Raskin, Jean-François (ed.) et al., Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 13660, 306-322 (2022).

MSC: 68V15 68Q60

Cite Review PDF

Full Text: DOI arXiv

Shimoda, Takumi; Kobayashi, Naoki; Sakayori, Ken; Sato, Ryosuke

Symbolic automatic relations and their applications to SMT and CHC solving. (English) Zbl 1497.68320

Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 405-428 (2021).

MSC: 68Q60 68P05 68Q45 68V15

Cite Review PDF

Full Text: DOI arXiv

Singher, Eytan; Itzhaky, Shachar

Theory exploration powered by deductive synthesis. (English) Zbl 1493.68388

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 125-148 (2021).

MSC: 68V15 68N30

Cite Review PDF

Full Text: DOI arXiv

OA License

De Angelis, Emanuele; Fioravanti, Fabio; Pettorossi, Alberto; Proietti, Maurizio

Removing algebraic data types from constrained Horn clauses using difference predicates. (English) Zbl 07614508

Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 83-102 (2020).

MSC: 68V15

Cite Review PDF

Full Text: DOI arXiv

De Angelis, Emanuele; Fioravanti, Fabio; Proietti, Maurizio

Transformational verification of Quicksort. (English) Zbl 07453193

Fribourg, Laurent (ed.) et al., Proceedings of the eighth international workshop on verification and program transformation and the seventh workshop on Horn clauses for verification and synthesis, VPT/HCVS 2020, Dublin, Ireland, April 25–26, 2020. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 320, 95-109 (2020).

MSC: 68N30 68Q60

Cite Review PDF

Full Text: arXiv Link

Echenim, M.; Peltier, N.

Combining induction and saturation-based theorem proving. (English) Zbl 1476.68300

J. Autom. Reasoning 64, No. 2, 253-294 (2020).

MSC: 68V15 03B35

Cite Review PDF

Full Text: DOI HAL

Johansson, Moa

Automated theory exploration for interactive theorem proving: an introduction to the Hipster system. (English) Zbl 1483.68484

Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 1-11 (2017).

MSC: 68V15

Cite Review PDF

Full Text: DOI

Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare

Model finding for recursive functions in SMT. (English) Zbl 1475.68448

Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 133-151 (2016).

MSC: 68V15 03B35 68Q60

Cite Review PDF

Full Text: DOI HAL

Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas

TIP: tons of inductive problems. (English) Zbl 1417.68179

Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 333-337 (2015).

MSC: 68T15

Cite Review PDF

Full Text: DOI Link

Found 12 Documents (Results 1–12)

Solving constrained Horn clauses over algebraic data types. (English) Zbl 1529.68167

Induction and Skolemization in saturation theorem proving. (English) Zbl 07601550

Analysis and transformation of constrained Horn clauses for program verification. (English) Zbl 1541.68215

Getting saturated with induction. (English) Zbl 1528.68391

Symbolic automatic relations and their applications to SMT and CHC solving. (English) Zbl 1497.68320

Theory exploration powered by deductive synthesis. (English) Zbl 1493.68388

Removing algebraic data types from constrained Horn clauses using difference predicates. (English) Zbl 07614508

Transformational verification of Quicksort. (English) Zbl 07453193

Combining induction and saturation-based theorem proving. (English) Zbl 1476.68300

Automated theory exploration for interactive theorem proving: an introduction to the Hipster system. (English) Zbl 1483.68484

Model finding for recursive functions in SMT. (English) Zbl 1475.68448

TIP: tons of inductive problems. (English) Zbl 1417.68179

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software