This post will collect applications of Binary Decision Diagram (BDD) in different fields. I only read briefly, so it could not be correct. digital circuit mapping: This paper and this...

paper link Paper summary This paper presents a framework / tool TRUSTEE that takes as input: 1. the ML model and 2. training dataset, and outputs: 1. a high-fidelity (i.e., correct) w...

After reinstalling Ubuntu 20.04, I encountered the same problem as I had in Ubuntu 22.04 when I was trying to connect external monitors. The default Nividia driver is nouveau, and it didn’t work. ...

I was using Ubuntu 22.04, but to be consistent with the environment on the server, I tried to reinstall Ubuntu 20.04. I first created a bootable USB stick with the Ubuntu built-in app “Startup Dis...

When learning the usage of fixed-point in Z3Py form this tutorial, I was not clear about the relations between using fixed-point engine such as Datalog and using quantifiers, then I found this Stac...

This post is a note of this paper. Why using probabilistic model to model human visions? Define scene to be the real environment (e.g., a picture), and define image to be the content percepted by...

yield and yield from This blog post gives a good introduction of how to use yield and yield from in Python. add local path with conda Similar to a normal IDE where a pro...

What is load balancing Load balancing refers to a set of strategies of packet forwarding to have optimal network utilization. Shortest path routing strategies does not always lead to good utiliza...

Online resources Decision procedures This book and associated slides teach how the decision procedure works in the SMT solver for different theories such as bit-vectors or linear real arthime...

What is SMT-LIBv2 SMT-LIBv2 is a standard for writing SMT constraints, its latest version v2.6 can be found here. Being a standard means any SMT solver such as z3 should be able to parse and chec...