اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Versatile, Sound Tool for Simplifying Definitions
54
0
0.0
(
0
)
تأليف
Alessandro Coglio
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old and new functions are equivalent. When appropriate it also generates termination and guard proofs for the new function. We explain how the tool is engineered so that these proofs will succeed. Examples illustrate its utility, in particular for program transformation in synthesis and verification.
قيم البحث
اقرأ أيضاً
The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial) security guarantees for smart contracts or require huge proof effort.
To address this challenge, we present SciviK, a versatile framework for specifying and verifying industrial-grade smart contracts. SciviKs versatile approach extends previous efforts with three key contributions: (i) an expressive annotation system enabling built-in directives for vulnerability pattern checking, neural-based loop invariant inference, and the verification of rich properties of real-world smart contracts (ii) a fine-grained model for the Ethereum Virtual Machine (EVM) that provides low-level execution semantics, (iii) an IR-level verification framework integrating both SMT solvers and the Coq proof assistant. We use SciviK to specify and verify security properties for 12 benchmark contracts and a real-world Decentralized Finance (DeFi) smart contract. Among all 158 specified security properties (in six types), 151 properties can be automatically verified within 2 seconds, five properties can be automatically verified after moderate modifications, and two properties are manually proved with around 200 lines of Coq code.
An interactive program verification tool usually requires users to write formal proofs in a theorem prover like Coq and Isabelle, which is an obstacle for most software engineers. In comparison, annotation verifiers can use assertions in source files
as hints for program verification but they themselves do not have a formal soundness proof. In this paper, we demonstrate VST-A, a foundationally sound annotation verifier for sequential C programs. On one hand, users can write high order assertion in C programs comments. On the other hand, separation logic proofs will be generated in the backend whose proof rules are formally proved sound w.r.t. CompCerts Clight semantics. Residue proof goals in Coq may be generated if some assertion entailments cannot be verified automatically.
Proteins are the active working horses in our body. These biomolecules perform all vital cellular functions from DNA replication and general biosynthesis to metabolic signaling and environmental sensing. While static 3D structures are now readily ava
ilable, observing the functional cycle of proteins - involving conformational changes and interactions - remains very challenging, e.g., due to ensemble averaging. However, time-resolved information is crucial to gain a mechanistic understanding of protein function. Single-molecule techniques such as FRET and force spectroscopies provide answers but can be limited by the required labelling, a narrow time bandwidth, and more. Here, we describe electrical nanopore detection as a tool for probing protein dynamics. With a time bandwidth ranging from microseconds to hours, it covers an exceptionally wide range of timescales that is very relevant for protein function. First, we discuss the working principle of label-free nanopore experiments, various pore designs, instrumentation, and the characteristics of nanopore signals. In the second part, we review a few nanopore experiments that solved research questions in protein science, and we compare nanopores to other single-molecule techniques. We hope to make electrical nanopore sensing more accessible to the biochemical community, and to inspire new creative solutions to resolve a variety of protein dynamics - one molecule at a time.
This review article describes the trapping of charged particles. The main principles of electromagnetic confinement of various species from elementary particles to heavy atoms are briefly described. The preparation and manipulation with trapped singl
e particles, as well as methods of frequency measurements, providing unprecedented precision, are discussed. Unique applications of Penning traps in fundamental physics are presented. Ultra-precise trap-measurements of masses and magnetic moments of elementary particles (electrons, positrons, protons and antiprotons) confirm CPT-conservation, and allow accurate determination of the fine-structure constant alpha and other fundamental constants. This together with the information on the unitarity of the quark-mixing matrix, derived from the trap-measurements of atomic masses, serves for assessment of the Standard Model of the physics world. Direct mass measurements of nuclides targeted to some advanced problems of astrophysics and nuclear physics are also presented.
Understanding and simulating how a quantum system interacts and exchanges information or energy with its surroundings is a ubiquitous problem, one which must be carefully addressed in order to establish a coherent framework to describe the dynamics a
nd thermodynamics of quantum systems. Significant effort has been invested in developing various methods for tackling this issue and in this Perspective we focus on one such technique, namely collision models, which have emerged as a remarkably flexible approach. We discuss their application to understanding non-Markovian dynamics and to studying the thermodynamics of quantum systems, two areas in which collision models have proven to be particularly insightful. Their simple structure endows them with extremely broad applicability which has spurred their recent experimental demonstrations. By focusing on these areas, our aim is to provide a succinct entry point to this remarkable framework.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
