close
1.

電子ブック

EB
edited by Ezio Bartocci, Rupak Majumdar
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9333
オンライン: http://dx.doi.org/10.1007/978-3-319-23820-3
目次情報: 続きを見る
Invited Papers
Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification
Twenty Years of Dynamic Software Model Checking
Explaining Heisenbugs
Regular Papers
Qualitative and Quantitative Monitoring of Spatio-Temporal Properties
Runtime Adaptation for Actor Systems
Robust Online Monitoring of Signal Temporal Logic
On Verifying The Hennessy-Milner Logic with Recursion at Runtime
Assuring the Guardians
A Case Study on Runtime Monitoring of an Autonomous Research Vehicle (ARV) System
Monitoring Electronic Exams
Monitoring Real Android Malware
Time-triggered Runtime Verification of Component-Based Multi-core Systems
Monitoring for a decidable fragment of MTL-R Runtime Verification Through Forward Chaining
Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information about the Environment
From First-Order Temporal Logic to Parametric Trace Slicing
R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems
A Hybrid Approach to Causality Analysis
Short Papers
Statistical Model Checking of Distributed Adaptive Real-Time Software
Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources
Runtime Verification for Hybrid Analysis Tools
Suggesting Edits to Explain Failing Traces
Tool Papers
StaRVOOrS - A Tool for Combined Static and Runtime Verification of Java
TIPEX: a tool chain for Timed Property Enforcement during eXecution
Tutorial Papers
Machine Learning Methods in Statistical Model Checking and System Design ? Tutorial
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial
LearnLib Tutorial - An Open Source Java Library for Active Automata Learning
Monitoring and Measuring Hybrid Behaviors - A Tutorial
Software Competitions
Second International Competition on Runtime Verification CRV 2015
Rigorous Examination of Reactive Systems: The RERS challenge 2015
Invited Papers
Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification
Twenty Years of Dynamic Software Model Checking
2.

電子ブック

EB
edited by Jesper Larsson Traff, Sascha Hunold, Francesco Versaci
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9233
オンライン: http://dx.doi.org/10.1007/978-3-662-48096-0
目次情報: 続きを見る
Concurrent Systems: Hybrid Object Implementations and Abortable Objects
Runtime-Aware Architectures
MPI Thread-Level Checking for MPI+OpenMP Applications
Event-Action Mappings for Parallel Tools Infrastructures
Low-Overhead Detection of Memory Access Patterns and Their Time Evolution
Automatic On-line Detection of MPI Application Structure with Event Flow Graphs
Online Automated Reliability Classification of Queueing Models for Streaming Processing Using Support Vector Machines
A Duplicate-Free State-Space Model for Optimal Task Scheduling
On the Heterogeneity Bias of Cost Matrices when Assessing Scheduling Algorithms
Hardware Round-Robin Scheduler for Single-ISA Asymmetric Multi-Core
Moody Scheduling for Speculative Parallelization
Allocating Jobs with Periodic Demands
A Multi?Level Hypergraph Partitioning Algorithm Using Rough Set Clustering
Non-preemptive Throughput Maximization for Speed-Scaling with Power-Down
Scheduling Tasks from Selfish Multi-tasks Agents
Locality and Balance for Communication-Aware Thread Mapping in Multicore Systems
Concurrent Priority Queues Are not Good Priority Schedulers
Load Balancing Prioritized Tasks via Work-Stealing
Optimizing Task Parallelism with Library-Semantics-Aware Compilation
Data Layout Optimization for Portable Performance
Automatic Data Layout Optimizations for GPUs
Performance Impacts with Reliable Parallel File Systems at Exascale Level
Rapid Tomographic Image Reconstruction via Large-Scale Parallelization
Software consolidation as an efficient energy and cost Saving Solution for a SaaS/PaaS Cloud Model
VMPlaceS A Generic Tool to Investigate and Compare VM Placement Algorithms
A Connectivity Model for Agreement in Dynamic Systems
DFEP: Distributed Funding-based Edge Partitioning
PR-STM: Priority Rule Based Software Transactions on the GPU
Leveraging MPI-3 Shared-Memory Extensions for Efficient PGAS Runtime Systems
A Practical Transactional Memory Interface
A Multicore Parallelization of Continuous Skyline Queries on Data Streams
A Fast and Scalable Graph Coloring Algorithm for Multi-core and Many-core Architectures
A Composable Deadlock-Free Approach to Object-Based Isolation
Scalable Data-Driven PageRank: Algorithms, System Issues & Lessons Learned
How Many Threads Will Be Too Many? On the Scalability of OpenMP Implementations
Efficient Nested Dissection for Multicore Architectures
Scheduling Trees of Malleable Tasks for Sparse Linear Algebra
Elastic Tasks: Unifying Task Parallelism and SPMD Parallelism with an Adaptive Runtime
Semi-discrete Matrix-Free Formulation of 3D Elastic Full Waveform Inversion Modeling
10,000 Performance Models per Minute - Scalability of the UG4 Simulation Framework
Exploiting Task-Based Parallelism in Bayesian Uncertainty Quantification
Parallelization of an Advection-Diffusion Problem Arising in Edge Plasma Physics Using Hybrid MPI/OpenMP Programming
Behavioral Non-Portability in Scientific Numeric Computing
Fast Parallel Suffix Array on the GPU
Effective Barrier Synchronization on Intel Xeon Phi Coprocessor
High Performance Multi-GPU SpMV for Multi-component PDE-based Applications
Accelerating Lattice Boltzmann Applications with OpenACC
High-Performance and Scalable Design of MPI-3 RMA on Xeon Phi Clusters
Improving Performance of Convolutional Neural Networks by Separable Filters on GPU
Iterative Sparse Triangular Solves for Preconditioning
Targeting the Parallella
Systematic Fusion of CUDA Kernels for Iterative Sparse Linear System Solvers
Efficient Execution of Multiple CUDA Applications using Transparent Suspend, Resume and Migration
Concurrent Systems: Hybrid Object Implementations and Abortable Objects
Runtime-Aware Architectures
MPI Thread-Level Checking for MPI+OpenMP Applications
3.

電子ブック

EB
edited by Tom Holvoet, Mirko Viroli
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9037
オンライン: http://dx.doi.org/10.1007/978-3-319-19282-6
目次情報: 続きを見る
Replica-Based High-Performance Tuple Space Computing
Investigating Fluid-Flow Semantics of Asynchronous Tuple-Based Process Languages for Collective Adaptive Systems
Logic Fragments: A Coordination Model Based on Logic Inference
Comingle: Distributed Logic Programming for Decentralized Mobile Ensembles
Dynamic Choreographies: Safe Runtime Updates of Distributed Applications
Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi
A Fix point-Based Calculus for Graph-Shaped Computational Fields
Take Command of Your Constraints!
A Labelled Semantics for Soft Concurrent Constraint Programming
Parallelisation and Application of AD3 as a Method for Solving Large Scale Combinatorial Auctions
Handling Agent Perception in Heterogeneous Distributed Systems: A Policy-Based Approach
Blending Event-Based and Multi-Agent Systems Around Coordination Abstractions
Klaim-DB: A Modeling Language for Distributed Database Applications
Open Transactions on Shared Memory
VISIRI - Distributed Complex Event Processing System for Handling Large Number of Queries
Replica-Based High-Performance Tuple Space Computing
Investigating Fluid-Flow Semantics of Asynchronous Tuple-Based Process Languages for Collective Adaptive Systems
Logic Fragments: A Coordination Model Based on Logic Inference
4.

電子ブック

EB
edited by Yunji Chen, Paolo Ienne, Qing Ji
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9231
オンライン: http://dx.doi.org/10.1007/978-3-319-23216-4
5.

電子ブック

EB
edited by Michael Butler, Sylvain Conchon, Fatiha Zaidi
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9407
オンライン: http://dx.doi.org/10.1007/978-3-319-25423-4
6.

電子ブック

EB
edited by Marcio Barros, Yvan Labiche
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9275
オンライン: http://dx.doi.org/10.1007/978-3-319-22183-0
7.

電子ブック

EB
edited by James Brodman, Peng Tu
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 8967
オンライン: http://dx.doi.org/10.1007/978-3-319-17473-0
目次情報: 続きを見る
Accelerator programming
Algorithms for parallelism
Compilers
Debugging
Vectorization
Accelerator programming
Algorithms for parallelism
Compilers
8.

電子ブック

EB
edited by Christian Terboven, Bronis R. de Supinski, Pablo Reble, Barbara M. Chapman, Matthias S. Muller
出版情報: Cham : Springer International Publishing : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9342
オンライン: http://dx.doi.org/10.1007/978-3-319-24595-9
9.

電子ブック

EB
edited by Christel Baier, Cesare Tinelli
出版情報: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2015
シリーズ名: Lecture Notes in Computer Science ; 9035
オンライン: http://dx.doi.org/10.1007/978-3-662-46681-0
目次情報: 続きを見る
Scalable Timing Analysis with Refinement
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
Verified Reachability Analysis of Continuous Systems
HyComp: An SMT-Based Model Checker for Hybrid Systems
C2E2: A Verification Tool for Stateflow Models
Non-cumulative Resource Analysis
Value Slice: A New Slicing Concept for Scalable Property Checking
A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
Commutativity of Reducers
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling
Analysis of Dynamic Process Networks
MULTIGAIN: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
vZ - An Optimizing SMT Solver
dReach: δ-Reachability Analysis for Hybrid Systems
Uppaal Stratego
BINSEC: Binary Code Analysis with Low-Level Regions
Insight: An Open Binary Analysis Framework
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
Symbolic Model-Checking Using ITS-Tools
Semantic Importance Sampling for Statistical Model Checking
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
FAUST2: Formal Abstractions of Uncountable-State Stochastic Processes
Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving
On Parallel Scalable Uniform SAT Witness Generation
Approximate Counting in SMT and Value Estimation for Probabilistic Programs
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
Stateless Model Checking for TSO and PSO
GPU Accelerated Strong and Branching Bisimilarity Checking
Fairness for Infinite-State Systems
Software Verification and Verifiable Witnesses
AProVE: Termination and Memory Safety of C Programs
Cascade
CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation
Framework for Embedded System Verification
Forester: Shape Analysis Using Tree Automata
MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings
Perentie: Modular Trace Refinement and Selective Value Tracking
Predator Hunting Party
SeaHorn: A Framework for Verifying C Programs
SMACK+Corral: A Modular Verifier
Ultimate Automizer with Array Interpolation
Ultimate Kojak with Memory Safety Checks
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches
FuncTion: An Abstract Domain Functor for Termination
Model Checking Gene Regulatory Networks
Symbolic Quantitative Robustness Analysis of Timed Automata
Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
Shield Synthesis: Runtime Enforcement for Reactive Systems
Verifying Concurrent Programs by Memory Unwinding
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs
An LTL Proof System for Runtime Verification
MARQ: Monitoring at Runtime with QEA
Parallel Explicit Model Checking for Generalized Bchi Automata
Limit Deterministic and Probabilistic Automata for LTL\GU
Saturation-Based Incremental LTL Model Checking with Inductive Proofs
Nested Antichains for WS1S
Sylvan: Multi-core Decision Diagrams
LTSmin: High-Performance Language-Independent Model Checking
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
Scalable Timing Analysis with Refinement
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
Verified Reachability Analysis of Continuous Systems