重載__bool__以實現符號執行
➤ 利用Python中的__bool__函數實現符號執行
✤ https://www.philipzucker.com/overload_bool/
本文介紹瞭如何通過重載Python中的__bool__函數來實現符號執行，以及利用Z3類別記錄Python代碼中的所有路徑的技巧，進行符號執行而無需傳統的流程。
+ 這篇文章對於如何在Python中進行符號執行提供了一個有趣的觀點，讓人對Python的應用產生更多想像。
+ 通過重載__bool__函數來實現符號執行，為語言處理和程式設計帶來了新的可能性，對於技術開發有啟發意義。
#符號執行 #Python #Z3

Readings shared December 16, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/16-readings_shared_12-16-24 #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math

'Lean-style' tactics in Knuckledragger. ~ Philip Zucker (@sandmouth.bsky.social). https://www.philipzucker.com/knuckle_lemma/ #Logic #SMT #Z3 #Python

I've completed "Claw Contraption" - Day 13 - Advent of Code 2024

I was looking for an excuse to use z3 again after the hailstones puzzle last year. Part 2 was one extra line.

https://github.com/jstanden/advent-of-code-python/blob/main/2024/day13.ipynb

Readings shared December 10, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/10-readings_shared_12-10-24 #Haskell #Python #Math #Logic #SMT #Z3 #Python #LLMs #Prolog #LogicProgramming

Dyckhoff intuitionistic propositional prover. ~ Philip Zucker (@sandmouth.bsky.social). https://www.philipzucker.com/ljt/ #Logic #SMT #Z3 #Python

Long Hei Matthew Lam from Monash University has given the oral presentation titled A Closer Look at Tool-based Logical Reasoning with #LLMs: The Choice of Tool Matters.

In this paper, he fills the gaps in the comparison between symbolic solvers, including #Z3, #Pyke, and
#Prover9 with #LLMs augmented.

I recently read a paper by Kleshnina and others and used it to teach myself some evolutionary game theory techniques.

This is a little obscure, so I'll thread below about why this topic matters for humans and the environment

https://nadiah.org/2024/11/20/kleshnina_2023

A nice little graph coloring problem, solved (or rather shown to be unsatisfiable) using #Z3 :
https://www.quora.com/Is-it-possible-for-all-the-vertices-of-a-dodecahedron-to-have-coloured-arrows-of-red-blue-and-green-pointing-to-and-from-them-along-their-respective-edges-but-an-edge-can-only-have-2-opposing-arrows-of-differing/answer/Mark-Gritter

My interpretation of what was asked: take the dodecahedron graph and make it directed (by doubling edges):
* Every vertex is the source of one red, one green, and one blue arrow.
* Every vertex is the target of one red, one green, and one blue arrow.
* The two opposite-direction arrows between vertices must be of different colors.

This approach to writing a #Z3 model is not gonna cut it. (Simulating the Rogue room generation algorithm and bogged down on the very first nested loop.) Am I gonna have to write my own DSL that is compiled to Z3?

There's got to be a better way to generate the model. My mental picture is as a tree where edges correspond to computational steps in the original algorithm -- maybe I can make that explicit in some form. Write successor functions for each possible state.

I'm trying to use Z3 to solve a logic puzzle, mostly as a chance to learn more about Z3. I'm stuck on a couple of things out of the gate:

How do people usually interact with Z3 in practice? Manually writing smtlib doesn't seem like it would scale. Do people use the Z3 bindings to Python, Java, etc. or are people using libraries to generate smtlib syntax which then gets fed in?

I'm looking at the TypeScript bindings. There's a "high level" set of bindings which seems incomplete (no support for datatype declarations, for example) and a "low level" set of bindings that seems more featureful. I get the vibe that the high level bindings aren't getting a lot of usage or maintenance. Can anyone confirm or give background here? Is TS simply the wrong language to use, or am I still likely to be writing Z3 in a modern-ish way by using the low level bindings?

I scheduled 35 lightning talks for ParslFest 2024 using Z3, replacing our traditional manual allocation.

I wrote up the experience in the README of this repo: https://github.com/benclifford/parslfest-2024-z3-schedule/

Lecturas compartidas el 21 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-21-de-mayo #ITP #Lean4 #IsabelleHOL #Coq #SMT #Z3 #FunctionalProgramming #Haskell #Python #Math

We have an exciting opportunity for a PostDoc
to work applying formal methods to enterprise systems: We will develop
techniques to detect faults and vulnerabilities in complex business-process-driven systems, contributing to
protecting critical workflows such as manufacturing, or logistics.

Apply until the 18th April 2024:
https://jobs.exeter.ac.uk/hrpr_webrecruitment/wrd/run/etrec179gf.open?WVID=171839ediw&LANG=USA&VACANCY_ID=386422ijTy

#Fedihire #Job #BPMN #BPL #FormalMethods #AcademicChatter #Security #ITP #Z3 #postdoc #unijobs
#ModelChecking #EnterpriseSecurity

#FlowersOnFriday In the last few days, the trees have become mostly bare, and our slide towards winter gathers momentum! Still lots of colour on shrubs and forbs, and still #flowers in the #garden though it takes a fairly tight focus in most beds! #florespondence #BloomScrolling #Alberta #z3 #October #Autumn
Geranium himalayense; Polemonium cf P. boreale Heavenly Habit; huge old Dasiphora fruticosa cv; Campanula persicifolia; Achillea millefolium

I like to read about #productivity and ways of improving how I work and make decisions. One of the skills that has helped me to provide more value to my internal customers and my team is something relatively simple: automating tedious tasks with #python. I guess I should do that more and add more tools to the toolbox like #machinelearning algorithms, #simpy, #z3 and others.