Zobrazeno 1 - 10
of 14
pro vyhledávání: '"Sascha Böhme"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 12, Issue 4 (2017)
Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-o
Externí odkaz:
https://doaj.org/article/8ed35a2262864b228ee90af20b5be12e
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642367410
TACAS
Logical Methods in Computer Science
TACAS
Logical Methods in Computer Science
Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9e5980f9e376129f16da9d8a5231dea7
https://doi.org/10.2168/lmcs-12(4:13)2016
https://doi.org/10.2168/lmcs-12(4:13)2016
Publikováno v:
Journal of Automated Reasoning. 51:109-128
Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::48de3ccf05370bdf0d16d64478b48779
https://doi.org/10.1007/s10817-013-9278-5
https://doi.org/10.1007/s10817-013-9278-5
Autor:
Mathias Fleury, Sascha Böhme, Steffen Smolka, Jasmin Christian Blanchette, Albert Steckermeier
Publikováno v:
Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩
Journal of Automated Reasoning, 2016, ⟨10.1007/s10817-015-9335-3⟩
Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩
Journal of Automated Reasoning, 2016, ⟨10.1007/s10817-015-9335-3⟩
International audience; Sledgehammer is a component of the Isabelle/HOL proof assistant that integrates external automatic theorem provers (ATPs) to discharge interactive proof obligations. As a safeguard against bugs, the proofs found by the externa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a313303b9bebaf8670ad0525bdd51120
https://hal.inria.fr/hal-01211748
https://hal.inria.fr/hal-01211748
Publikováno v:
it - Information Technology. 53:287-293
A certifying algorithm is an algorithm that produces, with each output, a certificate or witness that the particular output is correct. A user of a certifying algorithm inputs x, receives the output y and the certificate w, and then checks, either ma
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::969f3ab58300006847c94e015f0be53e
https://doi.org/10.1524/itit.2011.0655
https://doi.org/10.1524/itit.2011.0655
Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3f7584a4de89456a0f4ae5f83b61f152
Autor:
Sascha Böhme, Michal Moskal
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642224379
CADE
CADE
Software verification is one of the most prominent application areas for automatic reasoning systems, but their potential improvement is limited by shortage of good benchmarks. Current benchmarks are usually large but shallow, require decision proced
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::55989f350fe06f59245d986429612af1
https://doi.org/10.1007/978-3-642-22438-6_15
https://doi.org/10.1007/978-3-642-22438-6_15
Publikováno v:
Computer Aided Verification ISBN: 9783642221095
CAV
CAV
Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current verification tools and proving their correctness usually involves non-trivial mathematical theorems. Certifying algo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4f7c6bbcce9a6dad967f36298db6c192
https://doi.org/10.1007/978-3-642-22110-1_7
https://doi.org/10.1007/978-3-642-22110-1_7
Publikováno v:
Certified Programs and Proofs ISBN: 9783642253782
CPP
CPP
The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of unsatisfiability proofs for bit-vector theories in the theorem provers HOL4 and Isabelle/HOL. Our work shows that LCF
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::19da973d6c96fc76223a30e640335e02
https://doi.org/10.1007/978-3-642-25379-9_15
https://doi.org/10.1007/978-3-642-25379-9_15
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642224379
CADE
CADE
Sledgehammer is a component of Isabelle/HOL that employs firstorder automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that repla
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::088c486660fbd41d20279c483dda11b7
https://doi.org/10.1007/978-3-642-22438-6_11
https://doi.org/10.1007/978-3-642-22438-6_11