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
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...
Network Event Recognition
Springer Science and Business Media LLC - Tập 27 - Trang 213-251 - 2005
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...
Coverage-guided test generation for continuous and hybrid systems
Springer Science and Business Media LLC - Tập 34 - Trang 183-213 - 2009
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...
Performability assessment by model checking of Markov reward models
Springer Science and Business Media LLC - Tập 36 - Trang 1-36 - 2010
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...
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
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...
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs
Springer Science and Business Media LLC - - 2021
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...
SMT-based verification of program changes through summary repair
Springer Science and Business Media LLC - Tập 60 - Trang 350-380 - 2023
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...
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
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ẫ...
Vacuity in practice: temporal antecedent failure
Springer Science and Business Media LLC - Tập 46 - Trang 81-104 - 2015
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...
Achieving high coverage in hardware equivalence checking via concolic verification
Springer Science and Business Media LLC - Tập 60 - Trang 329-349 - 2023
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...
Tổng số: 485
- 1
- 2
- 3
- 4
- 5
- 6
- 10