RuleRunner技术报告

SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --

We present the derivation reduction problem for SLD-resolution, the undecidable problem of finding a finite subset of a set of clauses from which the whole set can be derived using SLD-resolution. We study the reducibility of various fragments of second-order Horn logic with particular applications in Inductive Logic Programming. We also discuss how these results extend to standard resolution.

全局SPACING限制（技术报告）

Global SPACING Constraint (Technical Report)

我们提出了一个新的全局空间约束，这是有用的建模事件，分布在时间上，如学习单位安排在一个学习计划或重复模式的音乐作品。首先，我们调查的约束和确定易处理的特殊情况下的理论性质。我们提出了有效的DC滤波算法，这些情况下。然后，我们通过实验评估所提出的算法的音乐作曲问题的性能，并证明我们的过滤算法优于国家的最先进的方法来解决这个问题。

多模态类型论的可靠且完备替换算法：技术报告

A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report

该技术报告配套多模态类型论替换算法相关论文，给出WSMTT完整定义、替换算法的可靠性与完备性详细证明，还补充SFMTT说明以保证文档自包含。

The Complexity of Synthesizing nop-Equipped Boolean Nets from g-Bounded Inputs (Technical Report)

Boolean Petri nets equipped with nop allow places and transitions to be independent by being related by nop. We characterize for any fixed natural number g the computational complexity of synthesizing nop-equipped Boolean Petri nets from labeled directed graphs whose states have at most g incoming and at most g outgoing arcs.

非确定性、概率性和量子效应通过事件结构的透镜（技术报告）

Non-deterministic, probabilistic, and quantum effects through the lens of event structures (Technical report)

本文通过事件结构框架研究非确定性、概率性和量子效应，提出了一种命令式操作框架并推导了正确性与充分性结果。

Query Answering for Rough EL Ontologies (Extended Technical Report)

Querying large datasets with incomplete and vague data is still a challenge. Ontology-based query answering extends standard database query answering by background knowledge from an ontology to augment incomplete data. We focus on ontologies written in rough description logics (DLs), which allow to represent vague knowledge by partitioning the domain of discourse into classes of indiscernible elements. In this paper, we extend the combined approach for ontology-based query answering to a variant of the DL EL augmented with rough concept constructors. We show that this extension preserves the g…

Pi-Calculus中的匹配（技术报告）

Matching in the Pi-Calculus (Technical Report)

我们研究是否，在π演算，匹配前缀-一个条件运算符测试两个名字（语法）平等-是通过其他运营商表示。在此之前，Carbone和Maffeis证明了匹配在相当强的要求下（保持和反射可观察性）是不可表达的。后来，Gorla开发了一套经过广泛测试的编码标准，允许更多的自由度（例如，它允许比较成功状态的可达性的演算，而不是直接翻译可观测量）。在本文中，我们仅使用Gorla放宽的要求，就匹配的不可表达性提供了相当强的分离结果。

重访模态立方体：无世界的语义学（技术报告）

The Modal Cube Revisited: Semantics without Worlds (Technical Report)

本文为模态立方体提出基于八值Nmatrices的非确定性语义框架，利用层级赋值捕获必然化，提供可靠完备判定程序，并解决非确定性下公理与语义条件对应关系的长期猜想。

生成地面反射的演算（技术报告）

A Calculus for Generating Ground Explanations (Technical Report)

我们提出了一个修改的叠加演算，这是为了产生解释为什么一组条款是可满足的。这个过程与溯因推理有关，产生的解释是在所谓的溯因常数上构造的子句。我们证明了存在的冗余消除规则的正确性和完整性的演算，并制定了一个充分条件，保证其终止，然后使用这个充分条件来证明，所有可能的解释可以产生无限的时间为几类条款集，包括许多感兴趣的SMT社区。我们提出了一个程序，生成一组解释，应该是有用的人类用户，并建议几个扩展这种新的方法结束。

用于Horn-Clause验证的析取插值（扩展技术报告）

Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

在软件验证的主要挑战之一是有效和精确的程序与过程和循环的组合分析。插值方法仍然是最有前途的技术之一，这样的验证，是密切相关的解决霍恩子句约束。我们引入了一个新的概念插值，析取插值，解决了更一般的一类问题，在一个步骤相比，以前的概念插值，如树插值或归纳序列的插值。我们目前的算法和复杂性建设的析取插值，以及它们的使用内的抽象细化循环。我们已经实现了霍恩条款验证算法，使用析取插值和评估他们的基准表示为霍恩条款的整数线性算术理论。

Complementing Büchi Automata with Ranker (Technical Report)

We present the tool Ranker for complementing Büchi automata (BAs). Ranker builds on our previous optimizations of rank-based BA complementation and pushes them even further using numerous heuristics to produce even smaller automata. Moreover, it contains novel optimizations of specialized constructions for complementing (i) inherently weak automata and (ii) semi-deterministic automata, all delivered in a robust tool. The optimizations significantly improve the usability of Ranker, as shown in an extensive experimental evaluation with real-world benchmarks, where Ranker produced in the majority…

A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report

Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approximate (i) arbitrary waitable events by abrupt program termination and (ii) busy-waiting for events by busy-waiting to be abruptly terminated. We propose a separation logic for modularly verifying termination (under fair scheduling) of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen.

From Stateless to Stateful Priorities: Technical Report

We present the notion of stateful priorities for imposing precise restrictions on system actions, in order to meet safety constraints. By using stateful priorities we are able to exclusively restrict erroneous system behavior as specified by the constraint, whereas safe system behavior remains unrestricted. Given a system modeled as a network of discrete automata and an error constraint, we present algorithms which use those inputs to synthesize stateful priorities. We present as well a network transformation which uses synthesized priorities for blocking all system actions leading to the inpu…

Automating Sized Type Inference for Complexity Analysis (Technical Report)

This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation, and constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to the choice of adopting an abstract index language and index polymorphism at higher ranks. A prototype implementation is availa…

The Complexity of Boolean State Separation (Technical Report)

For a Boolean type of nets $τ$, a transition system $A$ is synthesizeable into a $τ$-net $N$ if and only if distinct states of $A$ correspond to distinct markings of $N$, and $N$ prevents a transition firing if there is no related transition in $A$. The former property is called $τ$-state separation property ($τ$-SSP) while the latter -- $τ$-event/state separation property ($τ$-ESSP). $A$ is embeddable into the reachability graph of a $τ$-net $N$ if and only if $A$ has the $τ$-SSP. This paper presents a complete characterization of the computational complexity of \textsc{$τ$-SSP} for all Boole…

Technical Report: Using Loop Scopes with for-Loops

Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from while-loops to for-loops and also present sound loop unrolling rules for while- and for-loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for-loops to be treated as first-class citizens -- rather than the usual approach of transforming for-loops into while-loops -- which makes semi-automated proofs easier to follow for the user, who may need t…

Z3-Noodler：一种基于自动机的字符串求解器（技术报告）

Z3-Noodler: An Automata-based String Solver (Technical Report)

Z3-Noodler是一个基于自动机的字符串求解器，通过稳定化算法求解带正则约束的单词方程，在众多基准上超越现有求解器，并与其他求解器互补，适合作为求解器组合的候选。

Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)

Recursive algebraic data types (term algebras, ADTs) are one of the most well-studied theories in logic, and find application in contexts including functional programming, modelling languages, proof assistants, and verification. At this point, several state-of-the-art theorem provers and SMT solvers include tailor-made decision procedures for ADTs, and version 2.6 of the SMT-LIB standard includes support for ADTs. We study an extremely simple approach to decide satisfiability of ADT constraints, the reduction of ADT constraints to equisatisfiable constraints over uninterpreted functions (EUF) …

Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)

We present Behavioral Program Logic (BPL), a dynamic logic for trace properties that incorporates concepts from behavioral types and allows reasoning about non-functional properties within a sequent calculus. BPL uses behavioral modalities [s |- τ ], to verify statements s against behavioral specifications τ. Behavioral specifications generalize postconditions and behavioral types. They can be used to specify other static analyses, e.g., data flow analyses. This enables deductive reasoning about the results of multiple analyses on the same program, potentially implemented in different formalis…

技术报告：分布时间逻辑：结合正确性与估计质量

Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation

本文提出分布时间逻辑（DTL），用于描述部分可观测系统中涉及不确定性和可能性的属性，提供了一种安全的公式化方法及监控算法，并通过救援机器人应用案例验证。