miniblog.

Oct 3, 2017 at 23:15

The youngest user of Rosette is a highschooler who built a verifier that a type system is sound: https://www.youtube.com/watch?v=KpDyuMIb_E0&feature=youtu.be&t=9m20s (incredible!)

Dec 10, 2022 at 22:45

Computing optimal 8501 instructions for rotations using an SMT solver and Racket with Rosette:

Synthesizing optimal 8051 code — whitequark's lab notebook

Jul 13, 2018 at 19:05

Profiling symbolic execution by measuring the symbolic heap and the symbolic execution graph to ensure solver-aided tools are performant: https://2018.splashcon.org/event/splash-2018-oopsla-finding-code-that-explodes-under-symbolic-evaluation (Part of the remarkable Rosette project.)

Finding Code That Explodes Under Symbolic Evaluation (SPLASH 2018 - OOPSLA) - SPLASH 2018

PACMPL (OOPSLA) seeks contributions on all aspects of programming languages and software engineering. Authors of papers published in PACMPL will present their work at OOPSLA in Boston. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools (such as language front-ends, program analyses, and runtime systems), new techniques (such as methodologies, design processes, and ...

Feb 1, 2018 at 23:45

Going beyond QuickCheck: using an SMT solver (based on Rosette) to intelligently generate test inputs that are diverse and hit interesting code paths! https://youtu.be/Br16rvT_C00

Related Posts