Darren Valovcin

dblp:398/8675 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
1since 2021 · last 2025
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 1 · 1 since 2021

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Requirements engineering and software design · 87% Program verification · 13%

Topics — the 3 heaviest of 3, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Requirements engineering and software design › inconsistency management
completeness and consistency checking
0.912025
Completeness and Consistency of Tabular Requirements: An SMT-Based Verification Approach · IEEE Trans. Software Eng. 2025
Requirements engineering and software design
requirements specification
0.912025
Completeness and Consistency of Tabular Requirements: An SMT-Based Verification Approach · IEEE Trans. Software Eng. 2025
Program verification
SMT-based verification
0.312025
Completeness and Consistency of Tabular Requirements: An SMT-Based Verification Approach · IEEE Trans. Software Eng. 2025

Methods — techniques the papers use, named apart from their topics

unbounded encoding · 0.9bounded encoding · 0.9SMT solving · 0.9
YearPublicationVenuePosition
2025 Completeness and Consistency of Tabular Requirements: An SMT-Based Verification Approach
abstract
Tabular requirements assist with the specification of software requirements using an “if-then” paradigm and are supported by many tools. For example, the Requirements Table block in Simulink®supports writing executable specifications that can be used as test oracles to validate an implementation. But even before the development of an implementation, automatic checking of consistency and completeness of a Requirements Table can reveal errors in the specification. Fixing such errors earlier than in later development cycles avoids costly rework and additional testing efforts that would be required otherwise. As of version R2022a, Simulink®supports checking completeness and consistency of Requirements Tables when the requirements are stateless, that is, do not constrain behaviors over time. We overcome this limitation by considering Requirements Tables with both stateless and stateful requirements. This paper (i) formally defines the syntax and semantics of Requirements Tables, and their completeness and consistency, (ii) proposes eight encodings from two categories (namely, bounded and unbounded) that support stateful requirements, and (iii) implementsTheano, a solution supporting checking completeness and consistency using these encodings. We empirically assess the effectiveness and efficiency of our encodings in checking completeness and consistency by considering a benchmark of$160$Requirements Tables for a timeout of two hours. Our results show thatTheanocan check the completeness of all the Requirements Tables in our benchmark, it can detect the inconsistency of the Requirements Tables, but it can not confirm their consistency within the timeout. We also assessed the usefulness ofTheanoin checking the consistency and completeness of 14 versions of a Requirements Table for a practical example from the automotive domain. Across these 14 versions,Theanocould effectively detect two inconsistent and five incomplete Requirements Tables reporting a problem (inconsistency or incompleteness) for$50\%$(7 out of 14) versions of the Requirements Table.
Claudio Menghi, Eugene Balai, Darren Valovcin, Christoph Sticksel, Akshay Rajhans
IEEE Trans. Software Eng.3