Synthesizing optimal 8051 code with an SMT solver (2020)

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by PaulHoule on Saturday December 10, 2022 @01:05PM (#33934943)

Seems to me it would be better still the optimize the whole calculate the rotate is a part of (maybe you don’t really need one of those rotates) but that’s a lot tougher.

It is great to see SMT used for more real problems though!

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by pkkm on Saturday December 10, 2022 @02:44PM (#33936045)

That was my thought too. The author says that the memory usage grows extremely quickly; I wonder if there's a way to reduce it.

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by espadrine on Saturday December 10, 2022 @02:51PM (#33936121)

Isn‘t that what DeepMind tried to circumvent by using AlphaZero for AlphaTensor, to discover faster matrix multiplication techniques?

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by pkkm on Saturday December 10, 2022 @02:59PM (#33936214)

I think so. Their algorithms aren't known to be optimal though, just better than the previous ones.

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by mynameisash on Saturday December 10, 2022 @02:08PM (#33935695)

I would love to see more practical applications of SMT, particularly as intros to newbies.

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by __init on Saturday December 10, 2022 @04:29PM (#33937010)

Check out angr [1], a symbolic execution engine, and claripy [2], its frontend to SMT solvers like z3. Depending on your background, I probably wouldn't describe angr as "for newbies," but claripy is a very clean SMT interface!

[1] https://angr.io

[2] https://api.angr.io/claripy.html

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by c0742e9366 on Saturday December 10, 2022 @03:31PM (#33936505)

The (freely available) book "SAT/SMT by Example" [1] shows how a lot of different problems can be tackled with an SMT solver. I highly recommend it!

[1] https://sat-smt.codes/

[ Parent | on HN ]

Re:Synthesizing optimal 8051 code with an SMT solver (2020) by rurban on Sunday December 11, 2022 @10:56AM (#33944243)

How wrote something here: https://savannah.gnu.org/forum/forum.php?forum_id=9203

to find struct layouts for a binary format. Reverse engineering DWG

[ Parent | on HN ]