Springer Science and Business Media LLC

Công bố khoa học tiêu biểu

* Dữ liệu chỉ mang tính chất tham khảo

Sắp xếp:  
Isla: tích hợp ngữ nghĩa ISA quy mô đầy đủ và các mô hình đồng thời định lý (phiên bản mở rộng) Dịch bởi AI
Springer Science and Business Media LLC - - Trang 1-24 - 2023
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
Các thông số kiến trúc như Armv8-A và RISC-V là nền tảng cuối cùng cho việc xác minh phần mềm và tiêu chí chính xác cho việc xác minh phần cứng. Chúng nên xác định hành vi đồng thời của các chương trình theo thứ tự và mô hình bộ nhớ thư giãn cho phép, nhưng cho đến nay chưa có sự tích hợp giữa ngữ nghĩa tập lệnh kiến trúc quy mô đầy đủ (ISA) với các mô hình đồng thời định lý, cả về mặt toán học lẫ...... hiện toàn bộ
Verification of evolving software via component substitutability analysis
Springer Science and Business Media LLC - Tập 32 - Trang 235-266 - 2008
Sagar Chaki, Edmund Clarke, Natasha Sharygina, Nishant Sinha
This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning ...... hiện toàn bộ
Static detection of uncoalesced accesses in GPU programs
Springer Science and Business Media LLC - Tập 60 - Trang 1-32 - 2021
Rajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania
GPU programming has become popular due to the high computational capabilities of GPUs. Obtaining significant performance gains with GPU is however challenging and the programmer needs to be aware of various subtleties of the GPU architecture. One such subtlety lies in accessing GPU memory, where certain access patterns can lead to poor performance. Such access patterns are referred to as uncoalesc...... hiện toàn bộ
Model checking parameterized asynchronous shared-memory systems
Springer Science and Business Media LLC - Tập 50 - Trang 140-167 - 2016
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar
We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the case i...... hiện toàn bộ
Condensed state spaces for symmetrical Coloured Petri Nets
Springer Science and Business Media LLC - Tập 9 - Trang 7-40 - 1996
Kurt Jensen
This paper deals with state spaces. A state space is a directed graph with a node for each reachable state and an arc for each possible state change. We describe how symmetries of the modelled system can be exploited to obtain much more succinct state space analysis. The symmetries induce equivalence classes of states and equivalence classes of state changes. It is then possible to construct a con...... hiện toàn bộ
Floating Point Verification in HOL Light: The Exponential Function
Springer Science and Business Media LLC - Tập 16 - Trang 271-305 - 2000
John Harrison
Since they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computi...... hiện toàn bộ
Learning to verify branching time properties
Springer Science and Business Media LLC - - 2007
Abhay Vardhan, Mahesh Viswanathan
Efficient data race detection for async-finish parallelism
Springer Science and Business Media LLC - Tập 41 - Trang 321-347 - 2012
Raghavan Raman, Jisheng Zhao, Vivek Sarkar, Martin Vechev, Eran Yahav
A major productivity hurdle for parallel programming is the presence of data races. Data races can lead to all kinds of harmful program behaviors, including determinism violations and corrupted memory. However, runtime overheads of current dynamic data race detectors are still prohibitively large (often incurring slowdowns of 10× or more) for use in mainstream software development. In this paper, ...... hiện toàn bộ
Annotation guided collection of context-sensitive parallel execution profiles
Springer Science and Business Media LLC - Tập 54 - Trang 388-415 - 2019
Zachary Benavides, Keval Vora, Rajiv Gupta, Xiangyu Zhang
Studying the relative behavior of an application’s threads is critical to identifying performance bottlenecks and understanding their root causes. We present context-sensitive parallel (CSP) execution profiles, that capture the relative behavior of threads in terms of the user selected code regions they execute. CSPs can be analyzed to compute execution times spent by the application in interestin...... hiện toàn bộ
Preface of the special issue on the conference on formal methods in computer aided design 2018
Springer Science and Business Media LLC - Tập 57 - Trang 119-120 - 2021
Nikolaj Bjørner, Arie Gurfinkel
Tổng số: 485   
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 10