اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCompletely Automated Equivalence Proofs
100
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Verifying partial (i.e., termination-insensitive) equivalence of programs has significant practical applications in software development and education. Conventional equivalence verifiers typically rely on a combination of given relational summaries and suggested synchronization points; such information can be extremely difficult for programmers without a background in formal methods to provide for pairs of programs with dissimilar logic. In this work, we propose a completely automated verifier for determining partial equivalence, named Pequod. Pequod automatically synthesizes expressive proofs of equivalence conventionally only achievable via careful, manual constructions of product programs To do so, Pequod syntheses relational proofs for selected pairs of program paths and combines the per-path relational proofs to synthesize relational program invariants. To evaluate Pequod, we implemented it as a tool that targets Java Virtual Machine bytecode and applied it to verify the equivalence of hundreds of pairs of solutions submitted by students for problems hosted on popular online coding platforms, most of which could not be verified by existing techniques.
قيم البحث
اقرأ أيضاً
Nondeterminism in scheduling is the cardinal reason for difficulty in proving correctness of concurrent programs. A powerful proof strategy was recently proposed [6] to show the correctness of such programs. The approach captured data-flow dependenci
es among the instructions of an interleaved and error-free execution of threads. These data-flow dependencies were represented by an inductive data-flow graph (iDFG), which, in a nutshell, denotes a set of executions of the concurrent program that gave rise to the discovered data-flow dependencies. The iDFGs were further transformed in to alternative finite automatons (AFAs) in order to utilize efficient automata-theoretic tools to solve the problem. In this paper, we give a novel and efficient algorithm to directly construct AFAs that capture the data-flow dependencies in a concurrent program execution. We implemented the algorithm in a tool called ProofTraPar to prove the correctness of finite state cyclic programs under the sequentially consistent memory model. Our results are encouranging and compare favorably to existing state-of-the-art tools.
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restri
cted forms, or require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness. In this work, we introduce a novel automatic safety verifier of programs that maintain low-level data structures, named LTTP. LTTP synthesizes proofs of program safety represented as a grammar of a given programs control paths, annotated with invariants that relate program state at distinct points within its path of execution. LTTP synthesizes such proofs completely automatically, using a novel inductive-synthesis algorithm. We have implemented LTTP as a verifier for JVM bytecode and applied it to verify the safety of a collection of verification benchmarks. Our results demonstrate that LTTP can be applied to automatically verify the safety of programs that are beyond the scope of previously-developed verifiers.
Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual e
quivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence - it is sound and complete. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggis framework) functional languages.
Scalas type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Scala and similar languages. Unfortunately, it is not clear how DOT relat
es to any well-known type systems, and type soundness has only been established for very restricted subsets. In fact, important Scala features are known to break at least one key metatheoretic property such as environment narrowing or subtyping transitivity, which are usually required for a type soundness proof. First, and, perhaps surprisingly, we show how rich DOT calculi can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisens syntactic approach, is based on term rewriting, which does not a priori make a distinction between runtime and type assignment time. Second, we demonstrate how type soundness can be proved for advanced, polymorphic, type systems with respect to high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof in this style for System F<: and several extensions, including mutable references. Our proofs use only simple induction: another surprising result, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require co-inductive proof techniques. Third, we show how DOT-like calculi emerge as generalizations of F<:, exposing a rich design space of calculi with path-dependent types which we collectively call System D. Armed with insights from the definitional interpreter semantics, we also show how equivalent small-step semantics and soundness proofs in Wright-Felleisen-style can be derived for these systems.
This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Mult
iparty Session Types (MPST). Our approach is based upon the notion of a multiparty session type isomorphism, utilising a novel constructive realisation of service adapter code to establishing equivalence. We achieve this by employing trace semantics over a collection of local types and introducing meta abstractions over the syntax of global types. We develop a corresponding equational theory for MPST isomorphisms. The main motivation for this line of work is to define a type isomorphism that affords the assessment of whether two components/services are substitutables, modulo adaptation code given software components formalised as session types.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
