4 papers
Can LLM Aid in Solving Constraints with Inductive Definitions?
Weizhi Feng, Shidong Shen, Jiaxiang Liu +3
Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for…
Decision Procedure for A Theory of String Sequences
Denghang Hu, Taolue Chen, Philipp Rümmer +2
The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and pr…
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
Yedi Zhang, Fu Song, Taolue Chen +1
Reasoning about strategic abilities is key to AI systems comprising multiple agents, which provide a unified framework for formalizing various problems in game theory, social choic…
Towards Efficient Verification of Constant-Time Cryptographic Implementations
Luwei Cai, Fu Song, Taolue Chen
Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software secur…