Decision procedures in verification
2011/03/B/ST6/00346
Keywords
Descriptors
- ST6_7: Teoretyczne podstawy informatyki, w tym informatyka kwantowa
- ST1_1: Logika i podstawy matematyki
Panel
ST6 – Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems
Host institution
Uniwersytet Wrocławski, Wydział Matematyki i Informatyki
Voivodeship: dolnośląskie
Principal investigator (from the host institution)
Number of co-investigators in the project: 5
Call
OPUS 2 – announced on 2011-09-15
- Amount awarded
- 483 450 PLN
- Project start date
- 2012-08-31
- Project end date
- 2016-02-29
- Project duration
- 42 months (the same as in the proposal)
- Project status
- Project settled
Equipment purchased [PL]
- Komputer przenośny. Cost: 10 000 PLN
- Komputer z wydajnym procesorem i dużą pamięcią operacyjną. Cost: 10 000 PLN
Information in the final report
Publication in academic press/journals (6)
-
Two-variable Logic with Counting and Trees
- Authors:
- Witold Charatonik, Piotr Witkowski
- Academic press:
- ACM TRANSACTIONS ON COMPUTATIONAL LOGIC (year: 2016, volume: 17(4), pages: 31:1-31:27), Publisher: ACM
- Status:
- Published
- DOI:
- 10.1145/2983622 – link to the publication
-
Two-variable Logic with Counting and a Linear Order
- Authors:
- Witold Charatonik, Piotr Witkowski
- Academic press:
- Logical Methods in Computer Science (year: 2016, volume: 12(2:8), pages: 46053), Publisher: LOGICAL METHODS IN COMPUTER SCIENCE e.V.
- Status:
- Published
- DOI:
- 10.2168/LMCS-12(2:8)2016 – link to the publication
-
Bounded Model Checking of Pointer Programs Revisited
- Authors:
- Witold Charatonik, Piotr Witkowski
- Academic press:
- The Computing Research Repository (CoRR) (year: 2016, volume: abs/1602.09061, pages: 46046), Publisher: arXiv.org
- Status:
- Published
- DOI:
- link to the publication
-
Complexity of Two-Variable Logic on Finite Trees
- Authors:
- Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, James Worrell
- Academic press:
- ACM TRANSACTIONS ON COMPUTATIONAL LOGIC (year: 2016, volume: 17(4), pages: 32:1 - 32:38), Publisher: ACM
- Status:
- Published
- DOI:
- 10.1145/2996796 – link to the publication
-
Parameterized complexity of basic decision problems for tree automata
- Authors:
- Witold Charatonik and Agata Chorowska
- Academic press:
- International Journal of Computer Mathematics (year: 2013, volume: 90(6), pages: 1150-1170), Publisher: Taylor & Francis
- Status:
- Published
- DOI:
- 10.1080/00207160.2012.762451 – link to the publication
-
Theorem Proving for Classical Logic with Partial Functions by Reduction to Kleene Logic
- Authors:
- Hans de Nivelle
- Academic press:
- Journal of Logic and Computation (year: 2017, volume: 27(2), pages: 509-548), Publisher: Oxford University Press
- Status:
- Published
- DOI:
- 10.1093/logcom/exu071 – link to the publication
Articles in post-conference publications (5)
-
Complexity of Two-Variable Logic on Finite Trees
- Authors:
- Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, James Worrell
- Conference:
- Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013 (year: 2013, pages: 74-88), Publisher: Springer
- Date:
- conference July 8-12
- Status:
- Published
- DOI:
- link to the publication
-
Theorem Proving for Logic with Partial Functions by Reduction to Kleene Logic
- Authors:
- Hans de Nivelle
- Conference:
- Automated Reasoning in Quantified Non-Classical Logics ARQNL 2014 (year: 2014, pages: 71-85), Publisher: VSL Workshop Proceedings
- Date:
- conference 23 lipca 2014
- Status:
- Published
- DOI:
- link to the publication
-
Subsumption Algorithms for Three-Valued Geometric Resolution
- Authors:
- Hans de Nivelle
- Conference:
- International Joint Conference on Automated Reasoning (IJCAR) 2016 (year: 2016, pages: 257-272), Publisher: Springer International Pulblishing
- Date:
- conference 27 czerwca - 2 lipca 2016
- Status:
- Published
- DOI:
- link to the publication
-
Two-Variable Logic with Counting and Trees
- Authors:
- Witold Charatonik, Piotr Witkowski
- Conference:
- 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 (year: 2013, pages: 73-82), Publisher: IEEE Computer Society
- Date:
- conference June 25-28
- Status:
- Published
- DOI:
- link to the publication
-
Decidability of weak logics with deterministic transitive closure
- Authors:
- Witold Charatonik, Emanuel Kieroński, Filip Mazowiecki
- Conference:
- Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (year: 2014, pages: 29), Publisher: ACM
- Date:
- conference 14-18 lipca 2014
- Status:
- Published