Programming Constraint Services with Z3 (Nikolaj Bjørner, ISPRASOPEN-2019) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) (Batch edit: replace PCRE (\n\n)+(\n) with \2) |
||
(не показано 5 промежуточных версий этого же участника) | |||
* https://notebooks.azure.com/nbjorner/projects/z3examples {{----}} [[File:{{#setmainimage:Programming Constraint Services with Z3 (Nikolaj Bjørner, ISPRASOPEN-2019)!.jpg}}|center|640px]] {{LinksSection}} <!-- * [ Talks page on site] --> <!-- <blockquote>[©]</blockquote> --> {{fblink|2569531023299903}} {{vklink|1633}} <references/> <!-- topub --> [[Категория:ISPRASOPEN-2019]] [[Категория:Верификация]] {{stats|disqus_comments=0|refresh_time=2020-07-05T23:02:032021-08-31T16:33:47.836999350053|vimeo_plays=107|youtube_comments=0|youtube_plays=69}}47}} |
Текущая версия на 12:19, 4 сентября 2021
- Speaker
- Nikolaj Bjørner
Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet, there are many applications where satisfiability, and optionally a model or a proof, is insufficient. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. The tutorial describes, in an interactive way using jupyter notebooks, logical services from the point of view of the Satisfiability Modulo Theories solver Z3.
Video
Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.
Slides
Links
Plays:664 Comments:0