Zobrazeno 1 - 10
of 32
pro vyhledávání: '"Tjark Weber"'
Autor:
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Forsberg Gutkovas, Tjark Weber
Publikováno v:
Logical Methods in Computer Science, Vol Volume 17, Issue 1 (2021)
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these sys
Externí odkaz:
https://doaj.org/article/771b4fa2af15425eb60b77cb5c255282
Autor:
Joachim Parrow, Tjark Weber
Publikováno v:
Logical Methods in Computer Science, Vol Volume 12, Issue 2 (2016)
Respectful functions were introduced by Sangiorgi as a compositional tool to formulate short and clear bisimulation proofs. Usually, the larger the respectful function, the easier the bisimulation proof. In particular the largest respectful function,
Externí odkaz:
https://doaj.org/article/8cac6e3baa62481980bc0defd81e12a0
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 102, Iss Proc. SSV 2012, Pp 73-87 (2012)
In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. It is well-known that such an underspecified data-type semantics can be
Externí odkaz:
https://doaj.org/article/e670476537fd4d7d97383d5c7b96b325
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 332:1-17
Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In Isabelle/HOL, definable symbols are types and constants. The latter ma
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::baca214984b56f216cee16bf9e7b6e2a
https://doi.org/10.4204/eptcs.332.1
https://doi.org/10.4204/eptcs.332.1
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 11:221-259
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0306de7e23a492e34531774a1feb54ea
https://doi.org/10.3233/sat190123
https://doi.org/10.3233/sat190123
Autor:
Arve Gengelbach, Tjark Weber
Publikováno v:
Theoretical Aspects of Computing – ICTAC 2020 ISBN: 9783030642754
ICTAC
ICTAC
Logical frameworks are often equipped with an extensional mechanism to define new symbols. The definitional mechanism is expected to be conservative, i.e. it shall not introduce new theorems of the original language. The theorem proving framework Isa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6e71501660badd4a74af9fb5f7308356
https://doi.org/10.1007/978-3-030-64276-1_2
https://doi.org/10.1007/978-3-030-64276-1_2
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 9:207-242
The 2014 SMT Competition was held in conjunction with the SMT workshop, affiliated with the CAV, IJCAR, and SAT conferences at FLoC 2014, at the Vienna Summer of Logic in July 2014. Eighteen solvers participated from thirteen different research group
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::08de3e09d1e965734be654806c289bf3
https://doi.org/10.3233/sat190109
https://doi.org/10.3233/sat190109
Autor:
Arve Gengelbach, Tjark Weber
Publikováno v:
LSFA
Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ae76f13aff8d32c61eb8c028219b665a
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-368127
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-368127
Publikováno v:
Journal of Automated Reasoning. 55:61-90
After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::57e12cad02e983a26f349d94ced38f07
https://doi.org/10.1007/s10817-015-9328-2
https://doi.org/10.1007/s10817-015-9328-2
Publikováno v:
Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783319602240
FORTE
FORTE
Previous work on nominal transition systems explores strong bisimulation and a general kind of Hennessy-Milner logic with infinite but finitely supported conjunction, showing that it is remarkably expressive. In the present paper we treat weak bisimu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f853908c115c7b99499ca51fa99d4286
https://doi.org/10.1007/978-3-319-60225-7_13
https://doi.org/10.1007/978-3-319-60225-7_13