the ever increasing number and complexity of energy-bound devices (such as the ones used in Internet of things applications, smart phones, and mission critical systems) pose an important challenge on techniques to opt...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
the ever increasing number and complexity of energy-bound devices (such as the ones used in Internet of things applications, smart phones, and mission critical systems) pose an important challenge on techniques to optimize their energy consumption and to verify that they will perform their function within the available energy budget. In this work we address this challenge from the software point of view and propose a novel approach to estimating accurate parametric bounds on the energy consumed by program executions that are practical for their application to energy verification and optimization. Our approach divides a program into basic (branchless) blocks and performs a best effort modeling to estimate upper and lower bounds on the energy consumption for each block using an evolutionary algorithm. then it combines the obtained values according to the program control flow, using a safe static analysis, to infer functions that give both upper and lower bounds on the energy consumption of the whole program and its procedures as functions on input data sizes. We have tested our approach on (C-like) embedded programs running on the XMOS hardware platform. However, our method is general enough to be applied to other microprocessor architectures and programming languages. the bounds obtained by our prototype implementation on a set of benchmarks were always safe and quite accurate. this supports our hypothesis that our approach offers a good compromise between safety and accuracy, and can be applied in practice for energy verification and optimization.
this book constitutes the refereed proceedings of the 19thinternational Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2018, held in Los Angeles, CA, USA, in January 2018.;the 24 full ...
详细信息
ISBN:
(数字)9783319737218
ISBN:
(纸本)9783319737201
this book constitutes the refereed proceedings of the 19thinternational Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2018, held in Los Angeles, CA, USA, in January 2018.;the 24 full papers presented together withthe abstracts of 3 invited keynotes and 1 invited tutorial were carefully reviewed and selected from 43 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation, programsynthesis, static analysis, type systems, deductive methods, program certification, decision procedures, theorem proving, program certification, debugging techniques, programtransformation, optimization, and hybrid and cyber-physical systems.
the proceedings contain 19 papers. the special focus in this conference is on Model Checking Software. the topics include: An extension of TRIANGLE testbed with model-based testing;local data race freedom with non-mul...
ISBN:
(纸本)9783319941103
the proceedings contain 19 papers. the special focus in this conference is on Model Checking Software. the topics include: An extension of TRIANGLE testbed with model-based testing;local data race freedom with non-multi-copy atomicity;a comparative study of decision diagrams for real-time model checking;lazy reachability checking for timed automata with discrete variables;From SysML to model checkers via model transformation;genetic synthesis of concurrent code using model checking and statistical model checking;quantitative model checking for a controller design;modelling without a modelling language;context-updates analysis and refinement in chisel;efficient runtime verification of first-order temporal properties;program verification with separation logic;petri net reductions for counting markings;Improving generalization in software IC3;Star-topology decoupling in SPIN;joint forces for memory safety checking;Model-checking hyperLTL for pushdown systems;a branching time variant of CaRet.
this book constitutes the thoroughly refereed proceedings of the 19thinternationalsymposium on Static Analysis, SAS 2012, held in Deauville, France, in September 2012. the 25 revised full papers presented together w...
详细信息
ISBN:
(数字)9783642331251
ISBN:
(纸本)9783642331244
this book constitutes the thoroughly refereed proceedings of the 19thinternationalsymposium on Static Analysis, SAS 2012, held in Deauville, France, in September 2012. the 25 revised full papers presented together with 4 invited talks were selected from 62 submissions. the papers address all aspects of static analysis, including abstract domains, abstract interpretation, abstract testing, bug detection, data flow analysis, model checking, new applications, programtransformation, program verification, security analysis, theoretical frameworks, and type checking.
Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes ...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps s -> t and rewritings s -> *t (in zero or more steps) are defined for specific terms s and t by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules. We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.
Many transformation techniques developed for constraint logicprograms, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work ou...
详细信息
the proceedings contain 19 papers. the topics discussed include: on preferring and inspecting abductive models;declarative programming of user interfaces;huge data but small programs: visualization design via multiple...
ISBN:
(纸本)3540929940
the proceedings contain 19 papers. the topics discussed include: on preferring and inspecting abductive models;declarative programming of user interfaces;huge data but small programs: visualization design via multiple embedded DSLs;declarative network verification;operational semantics for declarative networking;ad hoc data and the token ambiguity problem;high level thread-based competitive or-parallelism in logtalk;implementing thread cancellation in multithreaded prolog systems;interoperating logic engines;high-level interaction with relational databases in logicprogramming;typed datalog;using bloom filters for large scale gene sequence analysis in Haskell;one table fits all;towards a complete scheme for tabled execution based on programtransformation;improving performance of conformant planners: static analysis of declarative planning domain specifications;and secure implementation of meta-predicates.
We propose a method, based on program analysis and transformation, for eliminating timing side channels in software code that implements security-critical applications. Our method takes as input the original program t...
详细信息
ISBN:
(纸本)9781450356992
We propose a method, based on program analysis and transformation, for eliminating timing side channels in software code that implements security-critical applications. Our method takes as input the original program together with a list of secret variables (e.g., cryptographic keys, security tokens, or passwords) and returns the transformed program as output. the transformed program is guaranteed to be functionally equivalent to the original program and free of both instruction- and cache-timing side channels. Specifically, we ensure that the number of CPU cycles taken to execute any path is independent of the secret data, and the cache behavior of memory accesses, in terms of hits and misses, is independent of the secret data. We have implemented our method in LLVM and validated its effectiveness on a large set of applications, which are cryptographic libraries with19,708 lines of C/C++ code in total. Our experiments show the method is both scalable for real applications and effective in eliminating timing side channels.
暂无评论