×

Found 430 Documents (Results 1–100)

Newest Citations Relevance
von Berg, Martin; Sanin, Arthur; Beierle, Christoph

Representing nonmonotonic inference based on c-representations as an SMT problem. (English) Zbl 07897227

Bouraoui, Zied (ed.) et al., Symbolic and quantitative approaches to reasoning with uncertainty. 17th European conference, ECSQARU 2023, Arras, France, September 19–22, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14294, 210-223 (2024).
MSC:  68T37
Cite Review PDF
Full Text: DOI
Eisenhofer, Clemens; Alassaf, Ruba; Rawson, Michael; Kovács, Laura

Non-classical logics in satisfiability modulo theories. (English) Zbl 07850736

Ramanayake, Revantha (ed.) et al., Automated reasoning with analytic tableaux and related methods. 32nd international conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14278, 24-36 (2023).
MSC:  68V15
Cite Review PDF
Full Text: DOI
OA License
Ekici, Burak; Viswanathan, Arjun; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark

Formal verification of bit-vector invertibility conditions in Coq. (English) Zbl 1540.68130

Sattler, Uli (ed.) et al., Frontiers of combining systems. 14th international symposium, Frocos 2023, Prague, Czech Republic, September 20–22, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14279, 41-59 (2023).
MSC:  68Q60 68V15
Cite Review PDF
Full Text: DOI arXiv
OA License
Fiedor, Tomáš; Holík, Lukáš; Hruška, Martin; Rogalewicz, Adam; Síč, Juraj; Vargovčík, Pavol

Reasoning about regular properties: a comparative study. (English) Zbl 07838493

Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 286-306 (2023).
MSC:  03B35 68V15
Cite Review PDF
Full Text: DOI arXiv
Tsai, Ming-Hsien; Fu, Yu-Fu; Liu, Jiaxiang; Shi, Xiaomu; Wang, Bow-Yaw; Yang, Bo-Yin

CoqCryptoLine: a verified model checker with certified results. (English) Zbl 07787555

Enea, Constantin (ed.) et al., Computer aided verification. 35th international conference, CAV 2023, Paris, France, July 17–22, 2023. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 13965, 227-240 (2023).
MSC:  68Q60 68V15 94A60
Cite Review PDF
Full Text: DOI
OA License
Korovin, Konstantin; Kovács, Laura; Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei

ALASCA: reasoning in quantified linear arithmetic. (English) Zbl 1543.68406

Sankaranarayanan, Sriram (ed.) et al., 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 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 13993, 647-665 (2023).
MSC:  68V15 03B35
Cite Review PDF
Full Text: DOI
OA License
Andreotti, Bruno; Lachnitt, Hanna; Barbosa, Haniel

Carcara: an efficient proof checker and elaborator for SMT proofs in the Alethe format. (English) Zbl 1543.68395

Sankaranarayanan, Sriram (ed.) et al., 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 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 13993, 367-386 (2023).
MSC:  68V15 68R07
Cite Review PDF
Full Text: DOI
OA License
Otoni, Rodrigo; Konnov, Igor; Kukovec, Jure; Eugster, Patrick; Sharygina, Natasha

Symbolic model checking for TLA+ made faster. (English) Zbl 1543.68227

Sankaranarayanan, Sriram (ed.) et al., 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 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 13993, 126-144 (2023).
MSC:  68Q60 68Q85 68W15
Cite Review PDF
Full Text: DOI
OA License
Arias, Jaime; Bae, Kyungmin; Olarte, Carlos; Ölveczky, Peter Csaba; Petrucci, Laure; Rømming, Fredrik

Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving. (English) Zbl 1541.68236

Gomes, Luis (ed.) et al., Application and theory of Petri nets and concurrency. 44th international conference, Petri NETS 2023, Lisbon, Portugal, June 25–30, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13929, 369-392 (2023).
MSC:  68Q85 68Q42 68Q55
Cite Review PDF
Full Text: DOI arXiv
Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel

Strategies in conditional narrowing modulo SMT plus axioms. (English) Zbl 1529.68129

Lopez-Garcia, Pedro (ed.) et al., Analysis, verification and transformation for declarative programming and intelligent systems. Essays dedicated to Manuel Hermenegildo on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 13160, 1-20 (2023).
MSC:  68Q42
Cite Review PDF
Full Text: DOI
Biere, Armin; Chowdhury, Md Solimul; Heule, Marijn J. H.; Kiesl, Benjamin; Whalen, Michael W.

Migrating solver state. (English) Zbl 07880748

Meel, Kuldeep S. (ed.) et al., 25th international conference on theory and applications of satisfiability testing, SAT 2022, Haifa, Israel, August 2–5, 2022. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 236, Article 27, 24 p. (2022).
MSC:  68Q25 68R07 68T20
Cite Review PDF
Full Text: DOI
De Angelis, Emanuele; V. K., Hari Govind

CHC-COMP 2022: competition report. (English) Zbl 07806143

Hamilton, Geoffrey W. (ed.) et al., Proceedings of the 9th workshop on Horn clauses for verification and synthesis and of the 10th international workshop on verification and program transformation, HCVS/VPT 2022, Munich, Germany, April 3, 2022. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 373, 44-62 (2022).
MSC:  68-XX 65-XX
Cite Review PDF
Full Text: arXiv Link
Amat, Nicolas; Dal Zilio, Silvano; Hujsa, Thomas

Property directed reachability for generalized Petri nets. (English) Zbl 07793113

Fisman, Dana (ed.) et al., 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 I. Cham: Springer. Lect. Notes Comput. Sci. 13243, 505-523 (2022).
MSC:  68Q85 68Q60
Cite Review PDF
Full Text: DOI arXiv
OA License
Cimatti, Alessandro; Griggio, Alberto; Lipparini, Enrico; Sebastiani, Roberto

Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. (English) Zbl 1522.68716

Bouajjani, Ahmed (ed.) et al., Automated technology for verification and analysis. 20th international symposium, ATVA 2022, virtual event, October 25–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13505, 137-153 (2022).
MSC:  68V15 55M25 90C30
Cite Review PDF
Full Text: DOI Link
Eleftheriadis, Charis; Kekatos, Nikolaos; Katsaros, Panagiotis; Tripakis, Stavros

On neural network equivalence checking using SMT solvers. (English) Zbl 07643438

Bogomolov, Sergiy (ed.) et al., Formal modeling and analysis of timed systems. 20th international conference, FORMATS 2022, Warsaw, Poland, September 13–15, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13465, 237-257 (2022).
MSC:  68Qxx
Cite Review PDF
Full Text: DOI arXiv
del Río, Tereso; England, Matthew

New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. (English) Zbl 1514.68323

Boulier, François (ed.) et al., Computer algebra in scientific computing. 24th international workshop, CASC 2022, Gebze, Turkey, August 22–26, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13366, 300-317 (2022).
MSC:  68W30 14P10 14Q30 68T20
Cite Review PDF
Full Text: DOI arXiv
Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare

Reasoning about vectors using an SMT theory of sequences. (English) Zbl 07628185

Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 125-143 (2022).
MSC:  68V15
Cite Review PDF
Full Text: DOI arXiv
OA License
Kremer, Gereon; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare

Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). (English) Zbl 07628183

Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 95-105 (2022).
MSC:  68V15
Cite Review PDF
Full Text: DOI
OA License
Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark

Flexible proof production in an industrial-strength SMT solver. (English) Zbl 07628179

Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 15-35 (2022).
MSC:  68V15
Cite Review PDF
Full Text: DOI
OA License
Berzish, Murphy; Kulczynski, Mitja; Mora, Federico; Manea, Florin; Day, Joel D.; Nowotka, Dirk; Ganesh, Vijay

An SMT solver for regular expressions and linear arithmetic over string length. (English) Zbl 1493.68182

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, 289-312 (2021).
MSC:  68Q45 68T20 68V20 68W32
Cite Review PDF
Full Text: DOI arXiv
OA License
Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick

Optimization modulo non-linear arithmetic via incremental linearization. (English) Zbl 07497924

Konev, Boris (ed.) et al., Frontiers of combining systems. 13th international symposium, FroCoS 2021, Birmingham, UK, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12941, 213-231 (2021).
MSC:  68Txx
Cite Review PDF
Full Text: DOI Link
Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark

Smt-Switch: a solver-agnostic C++ API for SMT solving. (English) Zbl 07495586

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 377-386 (2021).
MSC:  68Q25 68R07 68T20
Cite Review PDF
Full Text: DOI arXiv
Nummelin, Visa; Bentkamp, Alexander; Tourret, Sophie; Vukmirović, Petar

Superposition with first-class Booleans and inprocessing clausification. (English) Zbl 1540.03025

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 378-395 (2021).
MSC:  03B35 68V15
Cite Review PDF
Full Text: DOI
OA License
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca

Universal invariant checking of parametric systems with quantifier-free SMT reasoning. (English) Zbl 1542.68094

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 131-147 (2021).
MSC:  68Q60 03B70 68V15
Cite Review PDF
Full Text: DOI
OA License
Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang

Deductive verification of floating-point Java programs in KeY. (English) Zbl 1474.68186

Groote, Jan Friso (ed.) et al., 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 II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
MSC:  68Q60 65G50 68N15
Cite Review PDF
Full Text: DOI arXiv
OA License
Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei

Making theory reasoning simpler. (English) Zbl 1474.68060

Groote, Jan Friso (ed.) et al., 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 II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 164-180 (2021).
MSC:  68N30 68T20
Cite Review PDF
Full Text: DOI
OA License
Ghilardi, Silvio; Gianola, Alessandro; Kapur, Deepak

Interpolation and amalgamation for arrays with MaxDiff. (English) Zbl 07410429

Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 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. Cham: Springer. Lect. Notes Comput. Sci. 12650, 268-288 (2021).
MSC:  68Nxx 68Qxx
Cite Review PDF
Full Text: DOI arXiv
OA License

Filter Results by …

Document Type

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software