Succinct ordering and aggregation constraints in algebraic array theories. (English) Zbl 07870780
MSC:
68-XX
Found 63 Documents (Results 1–63)
Realizability modulo theories. (English) Zbl 07870778
MSC:
68-XX
On algebraic array theories. (English) Zbl 07803169
MSC:
68-XX
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).
A decision procedure for a theory of finite sets with finite integer intervals. (English) Zbl 07807741
Decision procedures for sequence theories. (English) Zbl 07787546
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, 18-40 (2023).
A solver for arrays with concatenation. (English) Zbl 07695707
MSC:
68V15
Counterexample-guided prophecy for model checking modulo the theory of arrays. (English) Zbl 07596574
MSC:
68Q60
Generalized arrays for Stainless frames. (English) Zbl 1498.68172
Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022).
NP satisfiability for arrays as powers. (English) Zbl 1498.68127
Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 301-318 (2022).
Time warps, from algebra to algorithms. (English) Zbl 07670526
Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 19th international conference, RAMiCS 2021, Marseille, France, November 2–5, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13027, 309-324 (2021).
MSC:
68Qxx
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).
Data abstraction: a general framework to handle program verification of data structures. (English) Zbl 1497.68108
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, 215-235 (2021).
Improving ENIGMA-style clause selection while learning from history. (English) Zbl 1540.68221
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, 543-561 (2021).
Incremental search for conflict and unit instances of quantified formulas with E-matching. (English) Zbl 1472.68184
Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 534-555 (2021).
MSC:
68T20
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).
Counterexample-guided prophecy for model checking modulo the theory of arrays. (English) Zbl 1467.68089
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 I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 113-132 (2021).
MSC:
68Q60
Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates. (English) Zbl 1543.03046
RustHorn: CHC-based verification for Rust programs. (English) Zbl 1508.68071
Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 484-514 (2020).
A learning-based approach to synthesizing invariants for incomplete verification engines. (English) Zbl 1468.68074
On invariant synthesis for parametric systems. (English) Zbl 1535.68143
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 385-405 (2019).
Satisfiability modulo theories. (English) Zbl 1392.68379
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 305-343 (2018).
MSC:
68T15
Decision procedure for entailment of symbolic heaps with arrays. (English) Zbl 1503.68045
Chang, Bor-Yuh Evan (ed.), Programming languages and systems. 15th Asian symposium, APLAS 2017, Suzhou, China, November 27–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10695, 169-189 (2017).
Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems. (English) Zbl 1419.68064
Property directed reachability for proving absence of concurrent modification errors. (English) Zbl 1484.68047
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, 209-227 (2017).
Adding decision procedures to SMT solvers using axioms with triggers. (English) Zbl 1356.68187
MSC:
68T15
03B35
A new acceleration-based combination framework for array properties. (English) Zbl 1471.68232
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, 169-185 (2015).
Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists. (English) Zbl 1322.68121
Nested refinements: a logic for duck typing. (English) Zbl 1321.68189
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 231-244 (2012).
Splitting via interpolants. (English) Zbl 1326.68091
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 186-201 (2012).
Modular instantiation schemes. (English) Zbl 1260.68370
MSC:
68T15
Schemata of SMT-problems. (English) Zbl 1333.03103
Brünnler, Kai (ed.) et al., Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4–8, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22118-7/pbk). Lecture Notes in Computer Science 6793. Lecture Notes in Artificial Intelligence, 27-42 (2011).
Towards complete reasoning about axiomatic specifications. (English) Zbl 1317.68117
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 278-293 (2011).
Beyond quantifier-free interpolation in extensions of Presburger arithmetic. (English) Zbl 1318.03045
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 88-102 (2011).
Satisfiability solving and model generation for quantified first-order logic formulas. (English) Zbl 1308.68039
Beckert, Bernhard (ed.) et al., Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28–30, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-18069-9/pbk). Lecture Notes in Computer Science 6528, 76-91 (2011).
Bugs, moles and skeletons: symbolic reasoning for software development. (English) Zbl 1291.68377
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 400-411 (2010).
MSC:
68T15
On hierarchical reasoning in combinations of theories. (English) Zbl 1291.03018
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 30-45 (2010).
MSC:
03B35
68T15
Inferring loop invariants using postconditions. (English) Zbl 1287.68108
Blass, Andreas (ed.) et al., Fields of logic and computation. Essays dedicated to Yuri Gurevich on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-15024-1/pbk). Lecture Notes in Computer Science 6300, 277-300 (2010).
MSC:
68Q60
Combination of convex theories: modularity, deduction completeness, and explanation. (English) Zbl 1192.68190
MSC:
68P05
Algorithmic analysis of array-accessing programs. (English) Zbl 1257.68102
Grädel, Erich (ed.) et al., Computer science logic. 23rd international workshop, CSL 2009, 18th annual conference of the EACSL, Coimbra, Portugal, September 7–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04026-9/pbk). Lecture Notes in Computer Science 5771, 86-101 (2009).
A logic-based framework for reasoning about composite data structures. (English) Zbl 1254.68146
Bravetti, Mario (ed.) et al., CONCUR 2009 – concurrency theory. 20th international conference, CONCUR 2009, Bologna, Italy, September 1–4, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04080-1/pbk). Lecture Notes in Computer Science 5710, 178-195 (2009).
Path feasibility analysis for string-manipulating programs. (English) Zbl 1234.68070
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, 307-321 (2009).
Lifting abstract interpreters to quantified logical domains. (English) Zbl 1295.68085
Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’08, San Francisco, CA, USA, January 07–12, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-689-9). 235-246 (2008).
Towards SMT model checking of array-based systems. (English) Zbl 1165.68406
Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 67-82 (2008).
MSC:
68Q60
68T15
On local reasoning in verification. (English) Zbl 1134.68410
Ramakrishnan, C. R. (ed.) et al., Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78799-0/pbk). Lecture Notes in Computer Science 4963, 265-281 (2008).
MSC:
68Q60
Applications of hierarchical reasoning in the verification of complex systems. (English) Zbl 1277.68135
Cook, B. (ed.) et al., Combined proceedings of the fourth workshop on pragmatics of decision procedures in automated reasoning (PDPAR 2006) and the first international workshop on probabilistic automata and logics (PaUL 2006), Seattle, WA, USA,
August 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 8, 39-54 (2007).
MSC:
68Q60
68T15
Invariant synthesis for combined theories. (English) Zbl 1132.68333
Cook, Byron (ed.) et al., Verification, model checking, and abstract interpretation. 8th international conference, VMCAI 2007, Nice, France, January 14–16, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-69735-0/pbk). Lecture Notes in Computer Science 4349, 378-394 (2007).
Filter Results by …
Document Type
- Journal Articles (29)
- Collection Articles (34)
all
top 5
Author
- Ghilardi, Silvio (6)
- Kuncak, Viktor (5)
- Sofronie-Stokkermans, Viorica (4)
- Barrett, Clark W. (3)
- Echenim, Mnacho (3)
- Hoenicke, Jochen (3)
- Jacobs, Swen (3)
- Padon, Oded (3)
- Peltier, Nicolas (3)
- Ranise, Silvio (3)
- Raya, Rodrigo (3)
- Sánchez, César (3)
- Alberti, Francesco (2)
- Bjørner, Nikolaj S. (2)
- Bonacina, Maria Paola (2)
- de Moura, Leonardo (2)
- Furia, Carlo Alberto (2)
- Garg, Pranav (2)
- Gianola, Alessandro (2)
- Griggio, Alberto (2)
- Ihlemann, Carsten (2)
- Irfan, Ahmed (2)
- Kapur, Deepak (2)
- Kimura, Daisuke (2)
- Kobayashi, Naoki (2)
- Madhusudan, Parthasarathy (2)
- Mann, Makai (2)
- Meyer, Bertrand (2)
- Neider, Daniel (2)
- Nicolini, Enrica (2)
- Rümmer, Philipp (2)
- Sánchez, Alejandro D. (2)
- Schindler, Tanja I. (2)
- Sharygina, Natasha (2)
- Tatsuta, Makoto (2)
- Zucchelli, Daniele (2)
- Alur, Rajeev (1)
- Appel, Andrew W. (1)
- Aravantinos, Vincent (1)
- Ballabriga, Clément (1)
- Beyer, Dirk (1)
- Biere, Armin (1)
- Bouajjani, Ahmed (1)
- Braine, Julien (1)
- Brillout, Angelo (1)
- Černý, Pavol (1)
- Chugh, Ravi (1)
- Conchon, Sylvain (1)
- Cristiá, Maximiliano (1)
- De Angelis, Emanuele (1)
- Dragoi, Cezara (1)
- Dross, Claire (1)
- Enea, Constantin (1)
- Ermis, Evren (1)
- Feldman, Yotam M. Y. (1)
- Fioravanti, Fabio (1)
- Forget, Julien (1)
- Fröhlich, Andreas M. (1)
- Frumkin, Asya (1)
- Gladisch, Christoph D. (1)
- Gonnord, Laure (1)
- Grelck, Clemens (1)
- Gu, Ming (1)
- Guatto, Adrien (1)
- Gulwani, Sumit (1)
- He, Fei (1)
- Henkel, Elisabeth (1)
- Henzinger, Thomas A. (1)
- Jeż, Artur (1)
- Jhala, Ranjit (1)
- Kanig, Johannes (1)
- Kirchner, Hélène (1)
- Kovásznai, Gergely (1)
- Kröning, Daniel (1)
- Lhoták, Ondřej (1)
- Lin, Anthony Widjaja (1)
- Löding, Christof (1)
- Lynch, Christopher A. (1)
- Majumdar, Rupak (1)
- Markgraf, Oliver (1)
- Matsushita, Yusuke (1)
- McCloskey, Bill (1)
- Mesnard, Fred (1)
- Metcalfe, George (1)
- Monniaux, David P. (1)
- Naso, Chiara (1)
- Nikolić, Đurica (1)
- Park, Daejun (1)
- Paskevich, Andrei (1)
- Payet, Étienne (1)
- Pettorossi, Alberto (1)
- Peuter, Dennis (1)
- Podelski, Andreas (1)
- Proietti, Maurizio (1)
- Ringeissen, Christophe (1)
- Rodríguez, Andoni (1)
- Rondon, Patrick Maxim (1)
- Rossi, Gianfranco (1)
- Ruiz, Jordy (1)
- Rybalchenko, Andrey (1)
- and 28 more Authors
all
top 5
Serial
- J. Autom. Reasoning (8)
- J. Log. Algebr. Methods Program. (3)
- J. Symb. Comput. (2)
- Form. Methods Syst. Des. (2)
- Ann. Math. Artif. Intell. (2)
- ACM Trans. Comput. Log. (2)
- Log. Methods Comput. Sci. (2)
- ACM Comput. Surv. (1)
- Acta Inf. (1)
- Inf. Process. Lett. (1)
- Theor. Comput. Sci. (1)
- Theory Comput. Syst. (1)
- Fundam. Inform. (1)
- J. Log. Algebr. Program. (1)
- Theory Pract. Log. Program. (1)
all
top 3
Software
- z3 (26)
- SIMPLIFY (11)
- CVC4 (9)
- SMT-LIB (6)
- Yices (6)
- Boogie (5)
- Dafny (5)
- ASTREE (4)
- Coq (4)
- GitHub (4)
- Mcmt (4)
- STP (4)
- Spacer (4)
- VCC (4)
- Boolector (3)
- Booster (3)
- ESC/Java (3)
- FOCI (3)
- FunArray (3)
- Houdini (3)
- MONA (3)
- SMTInterpol (3)
- SeaHorn (3)
- Spec# (3)
- cvc5 (3)
- iProver (3)
- Eiffel (2)
- IronFleet (2)
- Ivy (2)
- JayHorn (2)
- LiquidHaskell (2)
- MathSAT (2)
- REDLOG (2)
- SAFARI (2)
- SLAM (2)
- Slide (2)
- VAMPIRE (2)
- VeriFast (2)
- cvc3 (2)
- veriT (2)
- APL (1)
- AProVE (1)
- AXDInterpolator (1)
- Agda (1)
- Amphion (1)
- BAP (1)
- BLAST (1)
- Beaver (1)
- CLSAT (1)
- CPAchecker (1)
- CTIGAR (1)
- CUTE (1)
- Caduceus (1)
- Cassowary (1)
- Cayenne (1)
- Crust (1)
- Cubicle (1)
- Cyclone (1)
- DART (1)
- Darwin (1)
- DeepMath (1)
- E-Darvin (1)
- ECCE (1)
- ENIGMA (1)
- Easychair (1)
- FLATA (1)
- GASTAP (1)
- GPUVerify (1)
- GeoNames (1)
- H-PILoT (1)
- HAMPI (1)
- HIP (1)
- HOL-Boogie (1)
- Haskell (1)
- Infer (1)
- InvGen (1)
- IsaPlanner (1)
- Isabelle/HOL (1)
- Jahob (1)
- Julia Static Analyzer (1)
- KLEE (1)
- KRAKATOA (1)
- KRATOS (1)
- Lean (1)
- MathSAT5 (1)
- Matlab (1)
- MoCHi (1)
- MobileNetV2 (1)
- NASA PVS (1)
- NuSMV (1)
- OCaml (1)
- OSTRICH+ (1)
- OTTER (1)
- OpenSMT (1)
- PARTY (1)
- Pex (1)
- Predator (1)
- Princess (1)
- ProB (1)
- QPA (1)
- and 29 more Software Packages
