ICSE 2025
Sat 26 April - Sun 4 May 2025 Ottawa, Ontario, Canada
Wed 30 Apr 2025 16:15 - 16:30 at 103 - Formal Methods 2 Chair(s): Yi Li

Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, \emph{LTL learning} is the problem of synthesizing a specification, in \emph{linear temporal logic (LTL)}, that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called \emph{constrained LTL learning}, where the user, in addition to positive and negative examples, is given an option to specify one or more \emph{constraints} over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in a first-order relational logic and reduction to an instance of the \emph{maximal satisfiability (MaxSAT)} problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.

Wed 30 Apr

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 17:30
Formal Methods 2Research Track / New Ideas and Emerging Results (NIER) / Journal-first Papers at 103
Chair(s): Yi Li Nanyang Technological University
16:00
15m
Talk
ConsCS: Effective and Efficient Verification of Circom CircuitsFormal Methods
Research Track
Jinan Jiang The Hong Kong Polytechnic University, Xinghao Peng , Jinzhao Chu The Hong Kong Polytechnic University, Xiapu Luo Hong Kong Polytechnic University
16:15
15m
Talk
Constrained LTL Specification Learning from ExamplesFormal MethodsArtifact-FunctionalArtifact-AvailableArtifact-Reusable
Research Track
Changjian Zhang Carnegie Mellon University, Parv Kapoor Carnegie Mellon University, Ian Dardik Carnegie Mellon University, Leyi Cui Columbia University, Romulo Meira-Goes The Pennsylvania State University, David Garlan Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University
16:30
15m
Talk
LLM-aided Automatic Modeling for Security Protocol VerificationSecurityFormal Methods
Research Track
Ziyu Mao Zhejiang University, Jingyi Wang Zhejiang University, Jun Sun Singapore Management University, Shengchao Qin Xidian University, Jiawen Xiong East China Normal University
16:45
15m
Talk
Model Assisted Refinement of Metamorphic Relations for Scientific SoftwareFormal Methods
New Ideas and Emerging Results (NIER)
Clay Stevens Iowa State University, Katherine Kjeer Iowa State University, Ryan Richard Iowa State University, Edward Valeev Virginia Tech, Myra Cohen Iowa State University
17:00
15m
Talk
Precisely Extracting Complex Variable Values from Android AppsFormal Methods
Journal-first Papers
Marc Miltenberger Fraunhofer SIT; ATHENE, Steven Arzt Fraunhofer SIT; ATHENE
17:15
7m
Talk
A Unit Proofing Framework for Code-level Verification: A Research AgendaFormal Methods
New Ideas and Emerging Results (NIER)
Paschal Amusuo Purdue University, Parth Vinod Patil Purdue University, Owen Cochell Michigan State University, Taylor Le Lievre Purdue University, James C. Davis Purdue University
Pre-print
17:22
7m
Talk
Automated Testing Linguistic Capabilities of NLP Models
Journal-first Papers
Jaeseong Lee The University of Texas at Dallas, Simin Chen University of Texas at Dallas, Austin Mordahl University of Illinois Chicago, Cong Liu University of California, Riverside, Wei Yang UT Dallas, Shiyi Wei University of Texas at Dallas