Titlebook: Logic-Based Program Synthesis and Transformation; 30th International S Maribel Fernández Conference proceedings 2021 Springer Nature Switze

弯曲道理

Nominal Unification with Letrec and Environment-Variablesplicit environments could be treated in nominal unification and the use of abstract environments was restricted to nominal matching. This severely restricts the use of algorithms in applications. The following two restrictions permit a step forward and strongly improve the coverage of the applicatio

极小量

Terminating Non-disjoint Combined Unificationn practice in many fields such as automated reasoning, logic programming, declarative programming, and the formal analysis of security protocols. In this paper, we investigate the unification problem in the non-disjoint union of equational theories via the combination of hierarchical unification pro

ARBOR

JOT

Resourceful Program Synthesis from Graded Linear Typesnotion, enabling fine-grained, quantitative specification of data use in programs. The information provided by graded modal types appears to be useful for type-directed program synthesis, where these additional constraints can be used to prune the search space of candidate programs. We explore one o

FEMUR

Acetabulum

Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Studymbolic Execution (.) brings together concrete and symbolic execution to maximise the program coverage. . uses a constraint solver to solve the path conditions and generate new inputs to explore. In this paper we join these lines of research by introducing a model that combines . and . approaches. Th

较早

Translation of Interactive Datalog Programs for Microcontrollers to Finite State Machinesaches seem ideal to describe the behavior of the interactive systems. But managing input data and state is hard. With little choice of programming language, most code targeted at microcontrollers is written in imperative C or assembler..Microlog is a deductive database language with a strong logic f

Ringworm

似少年

Verification of Multiplayer Stochastic Games via Abstract Dependency Graphsh weighted transitions. This logic allows us to query about the existence of multiplayer strategies that aim to maximize the probability of game runs satisfying resource-bounded next and until logical operators, while requiring that the accumulated weight along the successful runs does not exceed a

强化

tween their entities, regarding semantic equivalence, is determined. In order to identify these correspondences several methods have been proposed in literature. The most common features that these methods employ are string-, lexical-, structure- and semantic-based features for which several approac