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

Other projects carried out by the institution »

Principal investigator (from the host institution)

prof. Witold Charatonik

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]

  1. Komputer przenośny. Cost: 10 000 PLN
  2. Komputer z wydajnym procesorem i dużą pamięcią operacyjną. Cost: 10 000 PLN

Information in the final report

Publication in academic press/journals (6)

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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)

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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

« New search

Graphic design and implementation: Jakub Piotrowski