Zobrazeno 1 - 10
of 143
pro vyhledávání: '"Helmut Veith"'
Publikováno v:
Language and Automata Theory and Applications ISBN: 9783030406073
LATA
LATA
We introduce a novel automata model, which we call pebble-intervals automata (PIA), and study its power and closure properties. PIAs are tailored for a decidable fragment of FO that is important for reasoning about structures that use data values fro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c40bb1fd4520c2de84c10c1f29273f2c
https://doi.org/10.1007/978-3-030-40608-0_14
https://doi.org/10.1007/978-3-030-40608-0_14
Publikováno v:
Formal Methods in System Design. 51:270-307
Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: FTDAs have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm
Publikováno v:
Formal Methods in System Design. 51:308-331
Secure multi-party computation (MPC) allows two or more distrusting parties to jointly evaluate a function over private inputs. For a long time considered to be a purely theoretical concept, MPC transitioned into a practical and powerful tool to buil
Publikováno v:
Distributed Computing
Parameterized model checking is the problem of deciding if a given formula holds irrespective of the number of participating processes. A standard approach for solving the parameterized model checking problem is to reduce it to model checking finitel
Publikováno v:
Journal of Automated Reasoning
Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb}
Autor:
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Publikováno v:
ACM SIGACT News. 47:53-64
Publikováno v:
Theoretical Computer Science. 605:62-79
The test specification language FQL describes relevant test goals as regular expressions over program locations, such that each matching test case has an execution path matching this expression. To specify not only test goals but entire suites, FQL d
Publikováno v:
EPiC Series in Computing.
Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NEXPTIME-complete, efficient ways of solving it would have many pract
Publikováno v:
Handbook of Model Checking ISBN: 9783319105741
Handbook of Model Checking
Handbook of Model Checking
Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical comput
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2138e559ba3bfe0631ae90b0a86e0ae1
https://doi.org/10.1007/978-3-319-10575-8_1
https://doi.org/10.1007/978-3-319-10575-8_1