Looking for Modeling questions in SMT, for students

[of...@ie.technion.ac.il]

I want to teach a basic subset of SMT-lib to students, and assign them modeling tasks in various theories.

Is anyone aware of such existing material ? 

Thanks, 

Ofer

[Markus Zimmermann]

We are doing a series on SAT, SMT and Symbolic Execution

- How to solve a 40-year-old riddle with a few lines of code https://symflower.com/en/company/blog/2021/smt-part-2/

- Finding test values: it's not black magic, it's simply math https://symflower.com/en/company/blog/2021/smt-part-1/
- Symflower's inner workings: the technology behind the curtain https://symflower.com/en/company/blog/2021/symbolic-execution/

Does that help? If yes, we have an open issue to do puzzles for SMTLIB so people can win t-shirts. Maybe we can collaborate on the puzzles?

I think i also have a talk on SMT if i should look for it let me know.

Cheers,

Markus

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/bc1ebaad-ae01-4451-b64f-83fca8ae0790n%40googlegroups.com.

[Aina Niemetz]

Ofer,

are you aware of Dennis Yurichev's SAT/SMT by example?
https://sat-smt.codes/

An excellent resource and I think exactly what you are looking for.

Cheers,
Aina

> --
> You received this message because you are subscribed to the Google
> Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to smt-lib+u...@googlegroups.com

> <mailto:smt-lib+u...@googlegroups.com>.

> To view this discussion on the web visit
> https://groups.google.com/d/msgid/smt-lib/bc1ebaad-ae01-4451-b64f-83fca8ae0790n%40googlegroups.com

> <https://groups.google.com/d/msgid/smt-lib/bc1ebaad-ae01-4451-b64f-83fca8ae0790n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Dennis Yurichev]

Hi all!

Thanks for mention.

I would be thankful for feedback and bug reports.

[Vijay Ganesh]

Yes, Dennis' books is excellent. I am using it as part of my SAT/SMT course.

Warm Regards,
Vijay Ganesh.
https://ece.uwaterloo.ca/~vganesh

________________________________________
From: smt...@googlegroups.com <smt...@googlegroups.com> on behalf of Dennis Yurichev <dennis....@gmail.com>
Sent: November 3, 2021 2:48 AM
To: SMT-LIB
Subject: Re: [smt-lib] Looking for Modeling questions in SMT, for students

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com<mailto:smt-lib+u...@googlegroups.com>.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/7dfb49b3-7144-49b2-8d01-fd3d7801c9d8n%40googlegroups.com<https://groups.google.com/d/msgid/smt-lib/7dfb49b3-7144-49b2-8d01-fd3d7801c9d8n%40googlegroups.com?utm_medium=email&utm_source=footer>.