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:  
Probabilistic black-box reachability checking (extended version)
Springer Science and Business Media LLC - Tập 54 - Trang 416-448 - 2019
Bernhard K. Aichernig, Martin Tappler
Model checking has a long-standing tradition in software verification. Given a system design it checks whether desired properties are satisfied. Unlike testing, it cannot be applied in a black-box setting. To overcome this limitation Peled et al.  introduced black-box checking, a combination of testing, model inference and model checking. The technique requires systems to be fully deterministic. F...... hiện toàn bộ
Network Event Recognition
Springer Science and Business Media LLC - Tập 27 - Trang 213-251 - 2005
Karthikeyan Bhargavan, Carl A. Gunter
Network protocols can be tested by capturing communication packets, assembling them into the high-level events, and comparing these to a finite state machine that describes the protocol standard. This process, which we call Network Event Recognition (NER), faces a number of challenges only partially addressed by existing systems. These include the ability to provide precise conformance with specif...... hiện toàn bộ
Coverage-guided test generation for continuous and hybrid systems
Springer Science and Business Media LLC - Tập 34 - Trang 183-213 - 2009
Thao Dang, Tarik Nahhal
In this paper, we describe a formal framework for conformance testing of continuous and hybrid systems, using the international standard ‘Formal Methods in Conformance Testing’ FMCT. We propose a novel test coverage measure for these systems, which is defined using the star discrepancy notion. This coverage measure is used to quantify the validation ‘completeness’. It is also used to guide input s...... hiện toàn bộ
Performability assessment by model checking of Markov reward models
Springer Science and Business Media LLC - Tập 36 - Trang 1-36 - 2010
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of perfor...... hiện toàn bộ
The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2
Springer Science and Business Media LLC - Tập 20 - Trang 91-106 - 2002
Ruben A. Gamboa
The powerlists data structure, created by Misra in the early 90s, is well suited to express recursive, data-parallel algorithms. Misra has shown how powerlists can be used to give simple descriptions to very complex algorithms, such as the Fast Fourier Transform (FFT). Such simplicity in presentation facilitates reasoning about the resulting algorithms, and in fact Misra has presented a stunningly...... hiện toàn bộ
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs
Springer Science and Business Media LLC - - 2021
Thomas Pani, Georg Weissenbacher, Florian Zuleger
We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs. To this end, we lift Jones’ rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. The compositionality (thread-modularity) of this framework allows us to reason about parameterized programs, i.e., programs that execute arbitrarily many concurren...... hiện toàn bộ
SMT-based verification of program changes through summary repair
Springer Science and Business Media LLC - Tập 60 - Trang 350-380 - 2023
Sepideh Asadi, Martin Blicha, Antti E. J. Hyvärinen, Grigory Fedyukovich, Natasha Sharygina
This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-a...... hiện toàn bộ
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ộ
Vacuity in practice: temporal antecedent failure
Springer Science and Business Media LLC - Tập 46 - Trang 81-104 - 2015
Shoham Ben-David, Fady Copty, Dana Fisman, Sitvanit Ruah
Different definitions of vacuity in temporal logic model checking have been suggested along the years. Examining them closely, however, reveals an interesting phenomenon. On the one hand, some of the definitions require high-complexity vacuity detection algorithms. On the other hand, studies in the literature report that not all vacuities detected in practical applications are considered a problem...... hiện toàn bộ
Achieving high coverage in hardware equivalence checking via concolic verification
Springer Science and Business Media LLC - Tập 60 - Trang 329-349 - 2023
Pritam Roy, Sagar Chaki
A concolic approach, called slec-cf, to find counterexamples (CEXs) to sequential equivalence between a high-level (e.g., SystemC) hardware description and an RTL (e.g., Verilog) is presented. slec-cf works by searching for CEXs over the possible values of a set of “control signals” in a depth-first lexicographic manner, and avoiding values that cannot be realized by any concrete input. In additio...... hiện toàn bộ
Tổng số: 485   
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 10