{"id":338,"date":"2022-07-08T06:40:35","date_gmt":"2022-07-08T06:40:35","guid":{"rendered":"https:\/\/easyconferences.eu\/ictcs2022\/?page_id=338"},"modified":"2023-05-25T06:17:01","modified_gmt":"2023-05-25T06:17:01","slug":"accepted-papers","status":"publish","type":"page","link":"https:\/\/easyconferences.eu\/cade2023\/accepted-papers\/","title":{"rendered":"Accepted Papers"},"content":{"rendered":"

[et_pb_section fb_built=”1″ next_background_color=”#ffffff” _builder_version=”4.16″ background_color=”#8c8c8c” top_divider_color=”#b53319″ bottom_divider_style=”arrow3″ global_colors_info=”{}”][et_pb_row _builder_version=”4.16″ custom_margin=”-26px|auto||auto||” global_colors_info=”{}”][et_pb_column type=”4_4″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_text _builder_version=”4.17.4″ global_colors_info=”{}”]<\/p>\n

Accepted Papers<\/span><\/h2>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=”1″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_row _builder_version=”4.16″ global_colors_info=”{}”][et_pb_column type=”4_4″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_text _builder_version=”4.21.0″ hover_enabled=”0″ inline_fonts=”Georgia” global_colors_info=”{}” sticky_enabled=”0″]<\/p>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
Verified Given Clause Procedures<\/td>\nJasmin Blanchette, Qi Qiu and Sophie Tourret<\/td>\n<\/tr>\n
Towards Fast Nominal Anti-Unification of Letrec-Expressions<\/td>\nManfred Schmidt-Schauss and Daniele Nantes-Sobrinho<\/td>\n<\/tr>\n
Confluence Criteria for Logically Constrained Rewrite Systems<\/td>\nJonas Sch\u00f6pf and Aart Middeldorp<\/td>\n<\/tr>\n
A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification<\/td>\nYu-Fang Chen, Philipp R\u00fcmmer and Wei-Lun Tsai<\/td>\n<\/tr>\n
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs<\/td>\nMarvin Brieger, Stefan Mitsch and Andr\u00e9 Platzer<\/td>\n<\/tr>\n
Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness<\/td>\nGuilherme Toledo, Yoni Zohar and Clark Barrett<\/td>\n<\/tr>\n
Superposition with Delayed Unification<\/td>\nAhmed Bhayat, Michael Rawson and Johannes Schoisswohl<\/td>\n<\/tr>\n
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus<\/td>\nAndrzej Indrzejczak and Yaroslav Petrukhin<\/td>\n<\/tr>\n
SAT-Based Subsumption Resolution<\/td>\nRobin Coutelier, Laura Kovacs, Michael Rawson and Jakob Rath<\/td>\n<\/tr>\n
An Isabelle\/HOL Formalization of the SCL(FOL) Calculus<\/td>\nMartin Bromberger, Martin Desharnais and Christoph Weidenbach<\/td>\n<\/tr>\n
Proving Termination of C Programs with Lists<\/td>\nJera Hensel and J\u00fcrgen Giesl<\/td>\n<\/tr>\n
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment<\/td>\nMaria Paola Bonacina, St\u00e9phane Graham-Lengrand and Christophe Vauthier<\/td>\n<\/tr>\n
Theorem Proving in Dependently-Typed Higher-Order Logic<\/td>\nColin Rothgang, Florian Rabe and Christoph Benzm\u00fcller<\/td>\n<\/tr>\n
Program Synthesis in Saturation<\/td>\nPetra Hozzov\u00e1, Laura Kov\u00e1cs, Chase Norman and Andrei Voronkov<\/td>\n<\/tr>\n
A more Pragmatic CDCL for IsaSAT and targetting LLVM<\/td>\nMathias Fleury and Peter Lammich<\/td>\n<\/tr>\n
Certified Core-Guided MaxSAT Solving<\/td>\nJeremias Berg, Bart Bogaerts, Jakob Nordstr\u00f6m, Andy Oertel and Dieter Vandesande<\/td>\n<\/tr>\n
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning<\/td>\nMartin Bromberger, Chaahat Jain and Christoph Weidenbach<\/td>\n<\/tr>\n
Iscalc: an Interactive Symbolic Computation Framework (System Description)<\/td>\nBohua Zhan, Yuheng Fan, Weiqiang Xiong and Runqing Xu<\/td>\n<\/tr>\n
Left-Linear Completion with AC Axioms<\/td>\nJohannes Niederhauser, Nao Hirokawa and Aart Middeldorp<\/td>\n<\/tr>\n
Choose your Colour: Tree Interpolation for Quantified Formulas in SMT<\/td>\nElisabeth Henkel, Tanja Schindler and Jochen Hoenicke<\/td>\n<\/tr>\n
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic<\/td>\nCl\u00e1udia Nalon, Ullrich Hustadt, Fabio Papacchini and Clare Dixon<\/td>\n<\/tr>\n
On Incremental Pre-processing for SMT<\/td>\nNikolaj Bjorner and Katalin Fazekas<\/td>\n<\/tr>\n
Proving Non-Termination by Acceleration Driven Clause Learning with LoAT \u2013 System Description<\/td>\nFlorian Frohn and J\u00fcrgen Giesl<\/td>\n<\/tr>\n
On P-interpolation in local theory extensions and applications to the study of\u00a0 interpolation in the\u00a0\u00a0 description logics EL, EL+<\/td>\nDennis Peuter, Viorica Sofronie-Stokkermans and Sebastian Thunert<\/td>\n<\/tr>\n
Incremental Rewriting Modulo SMT<\/td>\nGerald Whitters, Boon Loo, Vivek Nigam and Carolyn Talcott<\/td>\n<\/tr>\n
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs<\/td>\nJan-Christoph Kassing and J\u00fcrgen Giesl<\/td>\n<\/tr>\n
Formal Reasoning about Influence in Natural Sciences Experiments<\/td>\nFlorian Bruse, Martin Lange and S\u00f6ren M\u00f6ller<\/td>\n<\/tr>\n
Decidability of difference logic over the reals with uninterpreted unary predicates<\/td>\nBaptiste Vergain, Bernard Boigelot and Pascal Fontaine<\/td>\n<\/tr>\n
Reasoning about Regular Properties: A Comparative Study<\/td>\nLuk\u00e1\u0161 Hol\u00edk, Tomas Fiedor, Adam Rogalewicz, Pavol Vargov\u010d\u00edk, Martin Hruska and Juraj S\u00ed\u010d<\/td>\n<\/tr>\n
An Experimental Pipeline for Automated Reasoning in Natural Language<\/td>\nTanel Tammet, Priit J\u00e4rv, Martin Verrev and Dirk Draheim<\/td>\n<\/tr>\n
COOL 2 – A Generic Reasoner for Modal Fixpoint Logics<\/td>\nOliver G\u00f6rlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson and Lutz Schr\u00f6der<\/td>\n<\/tr>\n
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory<\/td>\nLukas Stevens<\/td>\n<\/tr>\n
\n

Verification of NP-hardness Reduction Functions for Exact Lattice Problems<\/p>\n<\/td>\n

Katharina Kreuzer and Tobias Nipkow<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"

Accepted Papers Verified Given Clause Procedures Jasmin Blanchette, Qi Qiu and Sophie Tourret Towards Fast Nominal Anti-Unification of Letrec-Expressions Manfred Schmidt-Schauss and Daniele Nantes-Sobrinho Confluence Criteria for Logically Constrained Rewrite Systems Jonas Sch\u00f6pf and Aart Middeldorp A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification Yu-Fang Chen, Philipp R\u00fcmmer and Wei-Lun Tsai Uniform […]<\/p>\n","protected":false},"author":3,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":""},"_links":{"self":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/338"}],"collection":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/comments?post=338"}],"version-history":[{"count":10,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/338\/revisions"}],"predecessor-version":[{"id":243765,"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/pages\/338\/revisions\/243765"}],"wp:attachment":[{"href":"https:\/\/easyconferences.eu\/cade2023\/wp-json\/wp\/v2\/media?parent=338"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}