A blockchain is a tamper-proof distributed transaction registry;first popularized by Bitcoin [1], it has now been extended to support storage of arbitrary state and computations in-ledger. Ethereum [2] and its smart c...
详细信息
ISBN:
(纸本)9781728115429
A blockchain is a tamper-proof distributed transaction registry;first popularized by Bitcoin [1], it has now been extended to support storage of arbitrary state and computations in-ledger. Ethereum [2] and its smart contract model have proven to be a very popular choice for this task, routinely managing assets valued in the billions. However, development of such contracts has been anything but easy. While formally specified, the Ethereum execution platform is based on a low-level machine, quite similar to assembly;semantics for contract operations such as call are quite complex, and the need for resource management creates unanticipated modes of failure. the dominant day-to-day programming platform for Ethereum is Solidity [3], an object-Oriented language that identifies contracts withobjects. While reasoning about Solidity programs is much easier than for their bytecode counterparts, it is not extent of challenges either, and moreover, Solidity lacks a source-level semantics, which forces developers to reason over output bytecode again. In this short paper we explore the main barriers to lift in order to achieve a principled compilation strategy for Solidity. We will review the standard concepts on verified and secure compilation, and frame them in the context of the Ethereum platform.
the proceedings contain 20 papers. the special focus in this conference is on Invited talk, formal UML modeling, Components and architecture, Joint discotec session, Timed process algebra, Timed and hybrid automata, P...
ISBN:
(纸本)3642134637
the proceedings contain 20 papers. the special focus in this conference is on Invited talk, formal UML modeling, Components and architecture, Joint discotec session, Timed process algebra, Timed and hybrid automata, Program logics and analysis and Reasoning about distributedsystems. the topics include: formal software verification;exploiting the hierarchical structure of rule-based specifications for decision planning;reactive semantics for distributed UML activities;statistical abstraction and model-checking of large heterogeneous systems;formal semantics and analysis of behavioral AADL models in real-time maude;testing probabilistic distributedsystems;specification and testing of e-commerce agents described by using UIOLTSs;testing attribute-based transactions in SOC;grouping nodes in wireless sensor networks using coalitional game theory;forgetting the time in timed process algebra;theory and implementation of a real-time extension to the π-calculus;fuzzy-timed automata;model checking of hybrid systems using shallow synchronization;heap-dependent expressions in separation logic;on-the-fly trace generation and textual trace analysis and their pplications to the analysis of cryptographic protocols;on efficient models for model checking message-passing distributed protocols and logics for contravariant simulations
the proceedings contain 16 papers. the topics discussed include: a reversible abstract machine and its space overhead;a small model theorem for rectangular hybrid automata networks;analysis of may-happen-in-parallel i...
ISBN:
(纸本)9783642307928
the proceedings contain 16 papers. the topics discussed include: a reversible abstract machine and its space overhead;a small model theorem for rectangular hybrid automata networks;analysis of may-happen-in-parallel in concurrent objects;behavioural equivalences over migrating processes with timers;checking soundness of business processes compositionally using symbolic observation graphs;beyond lassos: complete SMT-based bounded model checking for timed automata;conformance testing of boolean programs with multiple faults;knowledge-baseddistributed conflict resolution for multiparty interactions and priorities;modelling probabilistic wireless networks;noninterference via symbolic execution;defining distances for all process semantics;secure multi-execution through static program transformation;and TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs.
distributed decentralized implementation of systems of communicating processes raises non-trivial problems. Correct execution of multiparty interactions, subject to priority rules, requires sophisticated mechanisms fo...
详细信息
Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based B...
详细信息
object groups are collections of objects that perform collective work. We study a calculus withobject groups and develop a technique for the deadlock analysis of such systemsbased on abstract descriptions of method&...
详细信息
ISBN:
(纸本)9783642214615
object groups are collections of objects that perform collective work. We study a calculus withobject groups and develop a technique for the deadlock analysis of such systemsbased on abstract descriptions of method's behaviours.
the proceedings contain 21 papers. the special focus in this conference is on formal techniques for distributedsystems. the topics include: Keep it small, keep it real: efficient run-time verification of web service ...
ISBN:
(纸本)3642021379
the proceedings contain 21 papers. the special focus in this conference is on formal techniques for distributedsystems. the topics include: Keep it small, keep it real: efficient run-time verification of web service compositions;approximated context-sensitive analysis for parameterized verification;verification of parameterized systems with combinations of abstract domains;on model-checking optimistic replication algorithms;a software platform for timed mobility and timed interaction;modeling, validation, and verification of PCEP using the IF language;distinguing non-deterministic timed finite state machines;system model-based definition of modeling language semantics;typing component-based communication systems;epistemic logic for the applied Pi calculus;on process algebraic proof methods for fault tolerant distributedsystems;using first-order logic to reason about submodule construction;a model-checking approach for service component architectures;dynamic symbolic execution of distributed concurrent objects;checking the conformance of orchestrations with respect to choreographies in web services;a type graph model for java programs and conformance testing of network simulators based on metamorphic testing technique.
the proceedings contain 14 papers. the topics discussed include: guiding distributedsystems synthesis with language-based security policies;termination analysis of java bytecode;sessions and pipelines for structured ...
详细信息
ISBN:
(纸本)3540688625
the proceedings contain 14 papers. the topics discussed include: guiding distributedsystems synthesis with language-based security policies;termination analysis of java bytecode;sessions and pipelines for structured service programming;modular preservation of safety properties by cookie-based DoS-protection wrappers;mechanizing a correctness proof for a lock-free concurrent stack;symbolic step encoding for objectbased communicating state machines;modeling and model checking software product lines;semantic foundations and inference of non-null annotations;redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking;formal modeling of a generic middleware to ensure invariant properties;and a caller-side inline reference monitor for an object-oriented intermediate language.
In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this ...
详细信息
ISBN:
(纸本)9783642214615
In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this fact, and therefore may report it. Our approach uses knowledge properties that are precalculated based on model checking. As local knowledge is not always sufficient to monitor a global property in a concurrent system, we allow adding temporary synchronizations between two or more processes to achieve sufficient knowledge. Since synchronizations are expensive, we aim at minimizing their number using the knowledge analysis.
暂无评论