PV1 ⊧ S3 (versions: S3P, S3#, S3N)calculates the upper bound for the model count for a given formula

Links

• Project page: https://trinhmt.github.io/home/S3/
• Last commit date: - (Last version of the website was on 3 January 2018)

Related papers

• Inter-theory dependency analysis for SMT string solvers (OOPSLA '20, introduces the fourth version called S3N)
• Model Counting for Recursively-Defined Strings (CAV '17, introduces the third version called S3#)
• Progressive Reasoning over Recursively-Defined Strings (CAV '16, introduces the second version called S3P)
• S3 (CCS '14, introduces the first version called S3)

Related tools

• Earlier versions of the same tool: S3, S3P
• Later version of the same tool: S3N
• Other string model counters, compared to in the CAV '17 paper: SMC, ABC

ProVerB specific

• Markdown description: view/edit
• Reason for this entry: CAV 2017
• Contained in the ProVerB22 dataset (paper + artefact)