Found 92 Documents (Results 1–92)
Decidability of difference logic over the reals with uninterpreted unary predicates. (English) Zbl 07838507
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, 542-559 (2023).
Program synthesis in saturation. (English) Zbl 07838494
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, 307-324 (2023).
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).
Choose your colour: tree interpolation for quantified formulas in SMT. (English) Zbl 07838491
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, 248-265 (2023).
Fast approximations of quantifier elimination. (English) Zbl 07787548
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, 64-86 (2023).
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).
PFL: a probabilistic logic for fault trees. (English) Zbl 1529.68162
Chechik, Marsha (ed.) et al., Formal methods. 25th international symposium, FM 2023, Lübeck, Germany, March 6–10, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14000, 199-221 (2023).
Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability. (English) Zbl 1512.68428
Verified quadratic virtual substitution for real arithmetic. (English) Zbl 1521.68246
Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 200-217 (2021).
Automatic discovery of fair paths in infinite-state transition systems. (English) Zbl 1497.68290
Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 32-47 (2021).
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).
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).
Set constraints, pattern match analysis, and SMT. (English) Zbl 1503.68044
Bowman, William J. (ed.) et al., Trends in functional programming. 20th international symposium, TFP 2019, Vancouver, BC, Canada, June 12–14, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12053, 121-141 (2020).
Farkas-based tree interpolation. (English) Zbl 1474.68321
Pichardie, David (ed.) et al., Static analysis. 27th international symposium, SAS 2020, virtual event, November 18–20, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12389, 357-379 (2020).
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. (English) Zbl 1443.68104
A program logic for dependence analysis. (English) Zbl 1540.68057
Ahrendt, Wolfgang (ed.) et al., Integrated formal methods. 15th international conference, IFM 2019, Bergen, Norway, December 2–6, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11918, 83-100 (2019).
Satisfiability checking for mission-time LTL. (English) Zbl 1533.68168
Dillig, Isil (ed.) et al., Computer aided verification. 31st international conference, CAV 2019, New York City, NY, USA, July 15–18, 2019. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 11562, 3-22 (2019).
Computer-assisted proving of combinatorial conjectures over finite domains: a case study of a chess conjecture. (English) Zbl 1515.03060
Para-disagreement logics and their implementation through embedding in Coq and SMT. (English) Zbl 1439.03066
Carnielli, Walter (ed.) et al., Contradictions, from consistency to inconsistency. Cham: Springer. Trends Log. Stud. Log. Libr. 47, 139-158 (2018).
A generic framework for implicate generation modulo theories. (English) Zbl 1437.68190
Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 279-294 (2018).
Tactics and certificates in Meta Dedukti. (English) Zbl 1482.68266
Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 142-159 (2018).
Computing and estimating the volume of the solution space of SMT(LA) constraints. (English) Zbl 1398.68491
STLInspector: STL validation with guarantees. (English) Zbl 1494.68173
Majumdar, Rupak (ed.) et al., Computer aided verification. 29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10426, 225-232 (2017).
Counterexample-guided model synthesis. (English) Zbl 1452.68122
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 264-280 (2017).
Solving quantified linear arithmetic by counterexample-guided instantiation. (English) Zbl 1377.68138
Relational constraint solving in SMT. (English) Zbl 1494.68289
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 148-165 (2017).
Satisfiability modulo bounded checking. (English) Zbl 1494.68283
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 114-129 (2017).
Block-wise abstract interpretation by combining abstract domains with SMT. (English) Zbl 1484.68049
Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 310-329 (2017).
MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions. (English) Zbl 1428.68346
A decision procedure for separation logic in SMT. (English) Zbl 1398.68486
Artho, Cyrille (ed.) et al., Automated technology for verification and analysis. 14th international symposium, ATVA 2016, Chiba, Japan, October 17–20, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-46519-7/pbk; 978-3-319-46520-3/ebook). Lecture Notes in Computer Science 9938, 244-261 (2016).
MSC:
68T15
03B70
The incremental satisfiability problem for a two conjunctive normal form. (English) Zbl 1401.68119
Arrazola-Ramírez, José Ramón (ed.) et al., Selected papers of the 10th Latin American workshop on logic/languages, algorithms and new methods of reasoning (LANMR), Puebla, Mexico, August 15, 2016. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 328, 31-45 (2016).
Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers. (English) Zbl 1387.03007
Reviewer: Manfred Kerber (Birmingham)
A survey of satisfiability modulo theory. (English) Zbl 1453.68116
Gerdt, Vladimir P. (ed.) et al., Computer algebra in scientific computing. 18th international workshop, CASC 2016, Bucharest, Romania, September 19–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9890, 401-425 (2016).
Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms. (English) Zbl 1453.12002
Gerdt, Vladimir P. (ed.) et al., Computer algebra in scientific computing. 18th international workshop, CASC 2016, Bucharest, Romania, September 19–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9890, 193-211 (2016).
Finding finite models in multi-sorted first-order logic. (English) Zbl 1475.68447
Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 323-341 (2016).
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).
Adding decision procedures to SMT solvers using axioms with triggers. (English) Zbl 1356.68187
MSC:
68T15
03B35
Semi-intelligible Isar proofs from machine-generated proofs. (English) Zbl 1356.68178
MSC:
68T15
03B35
An experiment with satisfiability modulo SAT. (English) Zbl 1356.68208
MSC:
68T15
03B05
Adapting real quantifier elimination methods for conflict set computation. (English) Zbl 1471.68248
Lutz, Carsten (ed.) et al., Frontiers of combining systems. 10th international symposium, FroCoS 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9322, 151-166 (2015).
Quantifier-free equational logic and prime implicate generation. (English) Zbl 1465.68280
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 311-325 (2015).
Horn clause solvers for program verification. (English) Zbl 1465.68044
Beklemishev, Lev D. (ed.) et al., Fields of logic and computation II. Essays dedicated to Yuri Gurevich on the occasion of his 75th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9300, 24-51 (2015).
Two decades of Maude. (English) Zbl 1321.68007
Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 232-254 (2015).
Information flow in object-oriented software. (English) Zbl 1453.68027
Gupta, Gopal (ed.) et al., Logic-based program synthesis and transformation. 23rd international symposium, LOPSTR 2013, Madrid, Spain, September 18–19, 2013. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 8901, 19-37 (2014).
Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050
MSC:
03F05
Linear time-dependent constraints programming with MSVL. (English) Zbl 1298.68253
Reviewer: K. Subramani (Morgantown, WV)
Modular reasoning about heap paths via effectively propositional formulas. (English) Zbl 1284.68403
Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 385-396 (2014).
Abstract satisfaction. (English) Zbl 1284.68392
Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 139-150 (2014).
Witness runs for counter machines. (English) Zbl 1397.68122
Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 120-150 (2013).
Definability of accelerated relations in a theory of arrays and its applications. (English) Zbl 1397.68121
Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 23-39 (2013).
Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation. (English) Zbl 1253.68291
Efficient interpolant generation in satisfiability modulo linear integer arithmetic. (English) Zbl 1256.68138
Automated verification of shape, size and bag properties via user-defined predicates in separation logic. (English) Zbl 1243.68148
The TPTP typed first-order form with arithmetic. (English) Zbl 1352.68217
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 406-419 (2012).
MSC:
68T15
03B35
Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers. (English) Zbl 1352.68159
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 289-303 (2012).
Decidable logics combining heap structures and data. (English) Zbl 1284.68411
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’11, Austin, TX, USA, January 26–28, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0490-0). 611-622 (2011).
Expressing polymorphic types in a many-sorted language. (English) Zbl 1348.68215
Tinelli, Cesare (ed.) et al., Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5–7, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24363-9/pbk). Lecture Notes in Computer Science 6989. Lecture Notes in Artificial Intelligence, 87-102 (2011).
MSC:
68T15
03B70
Craig interpolation in the presence of non-linear constraints. (English) Zbl 1348.68141
Fahrenberg, Uli (ed.) et al., Formal modeling and analysis of timed systems. 9th international conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24309-7/pbk). Lecture Notes in Computer Science 6919, 240-255 (2011).
Canonized rewriting and ground AC completion modulo Shostak theories. (English) Zbl 1315.68219
Abdulla, Parosh Aziz (ed.) et al., Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 45-59 (2011).
Efficient generation of Craig interpolants in satisfiability modulo theories. (English) Zbl 1351.68247
Solving quantified verification conditions using satisfiability modulo theories. (English) Zbl 1184.68461
Complexity and algorithms for monomial and clausal predicate abstraction. (English) Zbl 1250.68194
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 214-229 (2009).
Ground interpolation for the theory of equality. (English) Zbl 1234.68257
Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 413-427 (2009).
Integrating external deduction tools with ACL2. (English) Zbl 1183.68558
MSC:
68T15
03B35
Encoding first order proofs in SMT. (English) Zbl 1277.03006
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 71-84 (2008).
MSC:
03B35
68T15
CC(X): semantic combination of congruence closure with solvable theories. (English) Zbl 1277.68240
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 51-69 (2008).
MSC:
68T15
03B35
Model-based theory combination. (English) Zbl 1277.03007
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 37-49 (2008).
E-matching for fun and profit. (English) Zbl 1277.68142
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 19-35 (2008).
Generating minimum transitivity constraints in P-time for deciding equality logic. (English) Zbl 1277.68146
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 3-17 (2008).
Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. (English) Zbl 1213.03021
Pfenning, Frank (ed.), Automated deduction – CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17–20, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73594-6/pbk). Lecture Notes in Computer Science 4603. Lecture Notes in Artificial Intelligence, 215-230 (2007).
Filter Results by …
Document Type
- Journal Articles (40)
- Collection Articles (52)
all
top 5
Author
- Tinelli, Cesare (7)
- Cimatti, Alessandro (6)
- Reynolds, Andrew (6)
- Griggio, Alberto (5)
- Barrett, Clark W. (4)
- Conchon, Sylvain (4)
- Sharygina, Natasha (4)
- Contejean, Evelyne (3)
- Fontaine, Pascal (3)
- Ghilardi, Silvio (3)
- Kuncak, Viktor (3)
- Sebastiani, Roberto (3)
- Tonetta, Stefano (3)
- Voronkov, Andrei (3)
- Alberti, Francesco (2)
- Bjørner, Nikolaj S. (2)
- Blanchette, Jasmin Christian (2)
- Brown, Christopher W. (2)
- Cruanes, Simon (2)
- de Moura, Leonardo (2)
- Echenim, Mnacho (2)
- Fuchs, Alexander (2)
- Goel, Amit (2)
- Grundy, Jim (2)
- Gurfinkel, Arie (2)
- Hoenicke, Jochen (2)
- Iguernelala, Mohamed (2)
- Kanig, Johannes (2)
- King, Tim (2)
- Kovács, Laura Ildikó (2)
- Krstic, Sava A. (2)
- Magnago, Enrico (2)
- Paskevich, Andrei (2)
- Peltier, Nicolas (2)
- Reger, Giles (2)
- Roveri, Marco (2)
- Tourret, Sophie (2)
- Ábrahám, Erika (1)
- Ansótegui, Carlos (1)
- Asadi, Sepideh (1)
- Banerjee, Anindya (1)
- Bansal, Kshitij (1)
- Baumgartner, Peter (1)
- Becker, Bernd (1)
- Beckert, Bernhard (1)
- Bentkamp, Alexander (1)
- Berendsen, Jasper (1)
- Biere, Armin (1)
- Blicha, Martin (1)
- Bobot, François (1)
- Bofill, Miquel (1)
- Böhme, Sascha (1)
- Boigelot, Bernard (1)
- Bongio, Jeremy (1)
- Bromberger, Martin (1)
- Bruns, Daniel (1)
- Bruttomesso, Roberto (1)
- Bubel, Richard (1)
- Cai, Shaowei (1)
- Cauderlier, Raphaël (1)
- Chen, Liqian (1)
- Chin, Wei-Ngan (1)
- Christ, Jürgen (1)
- Claessen, Koen (1)
- Clavel, Manuel (1)
- Cordwell, Katherine (1)
- Cousot, Patrick (1)
- Cousot, Radhia (1)
- Crossley, John Newsome (1)
- Davenport, James Harold (1)
- David, Cristina (1)
- de Ita Luna, Guillermo (1)
- De Oliveira, Diego Caminha B. (1)
- Déharbe, David (1)
- Demri, Stéphane P. (1)
- Deters, Morgan (1)
- Dobal, Pablo Federico (1)
- Dross, Claire (1)
- D’silva, Vijay (1)
- Duan, Zhenhua (1)
- Durán, Francisco (1)
- Eker, Steven (1)
- England, Matthew (1)
- Eraşcu, Mădălina (1)
- Eremondi, Joseph (1)
- Escobar, Santiago (1)
- Fedyukovich, Grigory (1)
- Fiedor, Tomáš (1)
- Finger, Marcelo (1)
- Fleury, Mathias (1)
- García-Contreras, Isabel (1)
- Ge, Cunjing (1)
- Ge, Yeting (1)
- Gianola, Alessandro (1)
- Guatto, Adrien (1)
- Hadarean, Liana (1)
- Hahn, Ernst Moritz (1)
- Hähnle, Reiner (1)
- Haller, Leopold (1)
- Hamadi, Youssef (1)
- and 133 more Authors
all
top 5
Serial
- Form. Methods Syst. Des. (7)
- Log. Methods Comput. Sci. (7)
- J. Autom. Reasoning (5)
- ACM Trans. Comput. Log. (3)
- Theor. Comput. Sci. (2)
- Sci. Comput. Program. (2)
- J. Symb. Comput. (2)
- Inf. Comput. (2)
- J. Appl. Log. (2)
- Fuzzy Sets Syst. (1)
- Inf. Sci. (1)
- Math. Struct. Comput. Sci. (1)
- Ann. Math. Artif. Intell. (1)
- Log. J. IGPL (1)
- J. Comb. Optim. (1)
- J. ACM (1)
- J. Satisf. Boolean Model. Comput. (1)
all
top 3
Software
- SMT-LIB (55)
- z3 (37)
- CVC4 (19)
- Yices (14)
- SIMPLIFY (12)
- Isabelle/HOL (10)
- TPTP (10)
- cvc3 (10)
- FOCI (9)
- VAMPIRE (7)
- Coq (6)
- MiniSat (6)
- E Theorem Prover (5)
- ESC/Java (5)
- Easychair (5)
- QEPCAD (5)
- SMT-RAT (5)
- SMTInterpol (5)
- Chaff (4)
- GitHub (4)
- MathSAT (4)
- REDLOG (4)
- Spacer (4)
- cvc5 (4)
- nuXmv (4)
- veriT (4)
- AVATAR (3)
- Alt-Ergo (3)
- Archive Formal Proofs (3)
- Isabelle (3)
- Mace4 (3)
- MathSAT5 (3)
- Orbital library (3)
- Princess (3)
- SPASS (3)
- SPASS+T (3)
- Sledgehammer (3)
- Spec# (3)
- Why3 (3)
- iProver (3)
- ACL2 (2)
- Boogie (2)
- Boolector (2)
- Booster (2)
- CLSAT (2)
- DPT (2)
- E-Darvin (2)
- Frama-C (2)
- HMC (2)
- HOL (2)
- HyTech (2)
- Ivy (2)
- JML (2)
- Leon (2)
- ML (2)
- MONA (2)
- Mcmt (2)
- Metis_ (2)
- Mjollnir (2)
- NuSMV (2)
- OCRA (2)
- OCaml (2)
- OpenSMT (2)
- PAGAI (2)
- Prover9 (2)
- QuickCheck (2)
- SOLAR (2)
- SYNRAC (2)
- StarExec (2)
- UCLID (2)
- Z (2)
- ABC (1)
- AMUSE (1)
- AProVE (1)
- ASTREE (1)
- AXDInterpolator (1)
- Antichains (1)
- Apron (1)
- BLAST (1)
- BOXES (1)
- Banshee (1)
- Beagle (1)
- CCASat (1)
- CCAnr (1)
- CIL (1)
- CMU Benchmarks (1)
- COMET (1)
- CVC (1)
- CakeML (1)
- CirQit2 (1)
- Cubicle (1)
- Darwin (1)
- Datalog (1)
- Denali (1)
- Eiffel (1)
- Emscripten (1)
- Esterel (1)
- FINDER (1)
- Find (1)
- Flyspeck (1)
- and 130 more Software Packages
