Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Articles by Topics
Topic D. - Software
Topic D.2 - SOFTWARE ENGINEERING
Topic D.2.4 - Software/Program Verification

J.-R. Abrial:
Formal Methods: Theory Becoming Practice
/jucs_13_5/formal_methods_theory_becoming
page 619 - 628
Vol.13 / Issue 5
M. Alférez, R.E. Lopez-Herrejón, A. Moreira, V. Amaral, A. Egyed:
Consistency Checking in Early Software Product Line Specifications - The VCC Approach
/jucs_20_5/consistency_checking_in_early
page 640 - 665
Vol.20 / Issue 5
M. Alpuente, M. del Mar Gallardo, E. Pimentel, A. Villanueva:
Verifying Real-Time Properties of tccp Programs
/jucs_12_11/verifying_real_time_properties
page 1551 - 1573
Vol.12 / Issue 11
D. B. Aredo:
A Framework for Semantics of UML Sequence Diagrams in PVS
/jucs_8_7/a_framework_for_semantics
page 674 - 697
Vol.8 / Issue 7
R. Banach:
Formal Methods
Guest Editorial
/jucs_13_5/formal_methods
page 593 - 601
Vol.13 / Issue 5
D. Batory, E. Börger:
Modularizing Theorems for Software Product Lines: The Jbook Case Study
/jucs_14_12/modularizing_theorems_for_software
page 2059 - 2082
Vol.14 / Issue 12
G. Bella:
What is Correctness of Security Protocols?
/jucs_14_12/what_is_correctness_of
page 2083 - 2107
Vol.14 / Issue 12
R. Berghammer, T. Hoffmann:
Modeling Sequences within the RelView System
/jucs_7_2/modeling_sequences_within_the
page 107 - 123
Vol.7 / Issue 2
A.D. Brucker, F. Rittinger, B. Wolff:
HOL-Z 2.0: A Proof Environment for Z-Specifications
/jucs_9_2/hol_z_2
page 152 - 172
Vol.9 / Issue 2
E. Börger, L. Mearelli:
Integrating ASMs into the Software Development Life Cycle
/jucs_3_5/integrating_asm
page 603 - 665
Vol.3 / Issue 5
E. Börger, O. Sörensen, B. Thalheim:
On Defining the Behavior of OR-joins in Business Process Models
/jucs_15_1/on_defining_the_behavior
page 3 - 32
Vol.15 / Issue 1
D. Cansell, D. Mery, S. Merz:
Diagram Refinements for the Design of Reactive Systems
/jucs_7_2/diagram_refinements_for_the
page 159 - 174
Vol.7 / Issue 2
P. Charuenporn, S. Intakosum:
Qos-Security Metrics Based on ITIL and COBIT Standard for Measurement Web Services
/jucs_18_6/qos_security_metrics_based
page 775 - 797
Vol.18 / Issue 6
E.M. Clarke, F. Lerda:
Model Checking: Software and Beyond
/jucs_13_5/model_checking_software_and
page 639 - 649
Vol.13 / Issue 5
J. Crossley, I. Poernomo:
Fred: An Approach to Generating Real, Correct, Reusable Programs from Proofs
/jucs_7_1/fred_an_approach_to
page 71 - 88
Vol.7 / Issue 1
D.-H. Dang, A.-H. Truong, M. Gogolla:
Checking the Conformance between Models Based on Scenario Synchronization
/jucs_16_17/checking_the_conformance_between
page 2293 - 2312
Vol.16 / Issue 17
D. Drusinsky:
Behavioral and Temporal Rule Checking for Gaussian Random Process – a Kalman Filter Example
/jucs_19_15/behavioral_and_temporal_rule
page 2198 - 2206
Vol.19 / Issue 15
D. Drusinsky:
Behavioral and Temporal Pattern Detection within Financial Data with Hidden Information
/jucs_18_14/behavioral_and_temporal_pattern
page 1950 - 1966
Vol.18 / Issue 14
D. Drusinsky:
On-line Monitoring of Metric Temporal Logic with Time-Series Constraints Using Alternating Finite Automata
/jucs_12_5/on_line_monitoring_of
page 482 - 498
Vol.12 / Issue 5
D. Drusinsky, M.-T. Shing:
Monitoring Temporal Logic Specifications Combined with Time Series Constraints
/jucs_9_11/monitoring_temporal_logic_specification
page 1261 - 1276
Vol.9 / Issue 11
J. Entrialgo, J. García, J.L. Díaz, D.F. García:
Tools and Stochastic Metrics for Debugging Temporal Behaviour of Real-Time Systems
/jucs_15_8/tools_and_stochastic_metrics
page 1563 - 1588
Vol.15 / Issue 8
F. Ferreira, R. Gheyi, P. Borba, G. Soares:
A Toolset for Checking SPL Refinements
/jucs_20_5/a_toolset_for_checking
page 587 - 614
Vol.20 / Issue 5
W. Fokkink, J. Pang:
Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
/jucs_12_8/variations_on_itai_rodeh
page 981 - 1006
Vol.12 / Issue 8
L. Fuentes, D. Jiménez, M. Pinto:
Development of Ambient Intelligence Applications using Components and Aspects
/jucs_12_3/development_of_ambient_intelligence
page 236 - 251
Vol.12 / Issue 3
S. Glesner:
Using Program Checking to Ensure the Correctness of Compiler Implementations
/jucs_9_3/using_program_checking_to
page 191 - 222
Vol.9 / Issue 3
L. Groves:
Reasoning about Nonblocking Concurrency
/jucs_15_1/reasoning_about_nonblocking_concurrency
page 72 - 111
Vol.15 / Issue 1
R. Halder, S. Pal, A. Cortesi:
Watermarking Techniques for Relational Databases: Survey, Classification and Comparison
/jucs_16_21/watermarking_techniques_for_relational
page 3164 - 3190
Vol.16 / Issue 21
A. Hall:
Realising the Benefits of Formal Methods
/jucs_13_5/realising_the_benefits_of
page 669 - 678
Vol.13 / Issue 5
C.L. Heitmeyer:
Formal Methods for Specifying, Validating, and Verifying Requirements
/jucs_13_5/formal_methods_for_specifying
page 607 - 618
Vol.13 / Issue 5
H. Hojjat, H. Nakhost, M. Sirjani:
Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP)
/jucs_13_13/integrating_module_checking_and
page 2076 - 2104
Vol.13 / Issue 13
M. J. Hornos:
FBT: A Tool for Applying Interval Logic Specifications to On-the-fly Model Checking
/jucs_10_11/fbt_a_tool_for
page 1498 - 1518
Vol.10 / Issue 11
C. B. Jones:
The Transition from VDL to VDM
/jucs_7_8/the_transition_from_VDL
page 631 - 640
Vol.7 / Issue 8
T. A. Junttila:
Computational Complexity of the Place/Transition-Net Symmetry Reduction Method
/jucs_7_4/computational_complexity_of_the
page 307 - 326
Vol.7 / Issue 4
F. Jurado, A.I. Molina, M.A. Redondo, M. Ortega, A. Giemza, L. Bollen, H.U. Hoppe:
Learning to Program with COALA, a Distributed Computer Assisted Environment
/jucs_15_7/learning_to_program_with
page 1472 - 1485
Vol.15 / Issue 7
Y. Kim, I. Kim, I. Kang, T. Kim, M. Sung:
Formal Modeling and Verification of Motor Drive Software for Networked Motion Control Systems
/jucs_20_14/formal_modeling_and_verification
page 1903 - 1925
Vol.20 / Issue 14
S.U.-J. Lee, G. Dobbie, J. Sun, L. Groves:
Formal Verification of Semistructured Data Models in PVS
/jucs_15_1/formal_verification_of_semistructured
page 241 - 272
Vol.15 / Issue 1
R. Malik, R. Mühlfeld:
A Case Study in Verification of UML Statecharts: the PROFIsafe Protocol
/jucs_9_2/a_case_study_in
page 138 - 151
Vol.9 / Issue 2
J.A. Mateo, M. del Carmen Ruiz, H. Maciá, J.J. Pardo:
Formal Study of Routing Protocols for Wireless Sensor Networks
/jucs_20_9/formal_study_of_routing
page 1373 - 1401
Vol.20 / Issue 9
L. Mearelli:
Refining an ASM Specification of the Production Cell to C++ Code
/jucs_3_5/production_cell
page 666 - 688
Vol.3 / Issue 5
H.-S. Min, S.-M. Chung, J.-Y. Choi:
Deriving System Behavior from UML State Machine Diagram: Applied to Missile Project
/jucs_19_1/deriving_system_behavior_from
page 53 - 77
Vol.19 / Issue 1
D. Mishra, A. Mishra:
A Global Software Inspection Process for Distributed Software Development
/jucs_18_19/a_global_software_inspection
page 2731 - 2746
Vol.18 / Issue 19
J. Mullins:
Nondeterministic Admissible Interference
/jucs_6_11/nondeterministic_admissible_interference
page 1054 - 1070
Vol.6 / Issue 11
D. Méry, S. Merz:
Specification and Refinement of Access Control
/jucs_13_8/specification_and_refinement_of
page 1073 - 1093
Vol.13 / Issue 8
T.V.N. Nguyen, F. Irigoin:
Alias Verification for Fortran Code Optimization
/jucs_9_3/alias_verification_for_fortran
page 270 - 297
Vol.9 / Issue 3
E.-R. Olderog, H. Dierks:
Moby/RT: A Tool for Specification and Verification of Real-Time Systems
/jucs_9_2/mobyrt_a_tool_for
page 88 - 105
Vol.9 / Issue 2
A. Puccetti:
Static Analysis of the XEN Kernel using Frama-C
/jucs_16_4/static_analysis_of_the
page 543 - 553
Vol.16 / Issue 4
S.K. Rajamani:
Software Is More Than Code
/jucs_13_5/software_is_more_than
page 602 - 606
Vol.13 / Issue 5
W. Reif, G. Schellhorn, T. Vollmer, J. Ruf:
Correctness of Efficient Real-Time Model Checking
/jucs_7_2/correctness_of_efficient_real
page 194 - 209
Vol.7 / Issue 2
J. Rothe, H. Tews, B. Jacobs:
The Coalgebraic Class Specification Language CCSL
/jucs_7_2/the_coalgebraic_class_specification
page 175 - 193
Vol.7 / Issue 2
J. Rushby:
Automated Formal Methods Enter the Mainstream
/jucs_13_5/automated_formal_methods_enter
page 650 - 660
Vol.13 / Issue 5
H. Sabouri, R. Khosravi:
Modeling and Verification of Reconfigurable Actor Families
/jucs_19_2/modeling_and_verification_of
page 207 - 232
Vol.19 / Issue 2
S. Sasaki, T. Nishihara, D. Ando, M. Fujita:
Hardware/Software Co-design and Verification Methodology from System Level Based on System Dependence Graph
/jucs_13_13/hardware_software_codesign_and
page 1972 - 2001
Vol.13 / Issue 13
G. Schellhorn:
Verification of ASM Refinements Using Generalized Forward Simulation
/jucs_7_11/verification_of_asm_refinements
page 952 - 979
Vol.7 / Issue 11
G. Schellhorn:
ASM Refinement Preserving Invariants
/jucs_14_12/asm_refinement_preserving_invariants
page 1929 - 1948
Vol.14 / Issue 12
M. Sirjani, F.S. de Boer, A. Movaghar:
Modular Verification of a Component-Based Actor Language
/jucs_11_10/modular_verificatin_of_a
page 1695 - 1717
Vol.11 / Issue 10
M. Sirjani, A. Movaghar, A. Shali, F. S. de Boer:
Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models
/jucs_11_6/model_checking_automated_abstraction
page 1054 - 1082
Vol.11 / Issue 6
A. Slissenko, P. Vasilyev:
Simulation of Timed Abstract State Machines with Predicate Logic Model-Checking
/jucs_14_12/simulation_of_timed_abstract
page 1984 - 2006
Vol.14 / Issue 12
G. Smith, C. Fidge:
Incremental Development of Real-Time Requirements: The Light Control Case Study
/jucs_6_7/incremental_development_of_real
page 704 - 730
Vol.6 / Issue 7
K. Strötmann:
The Constrained Shortest Path Problem: A Case Study in Using ASMs
/jucs_3_4/shortest_path_problem
page 304 - 319
Vol.3 / Issue 4
R. F. Stärk, S. Nanchen:
A Logic for Abstract State Machines
/jucs_7_11/a_logic_for_abstract
page 980 - 1005
Vol.7 / Issue 11
W. Sun, E. Song, P.C. Grabow, D.M. Simmonds:
Toward an Integrated Tool Environment for Static Analysis of UML Class and Sequence Models
/jucs_16_17/toward_an_integrated_tool
page 2435 - 2454
Vol.16 / Issue 17
L.-M. Traonouez, D. Lime, O.H. Roux:
Parametric Model-Checking of Stopwatch Petri Nets
/jucs_15_17/parametric_model_checking_of
page 3273 - 3304
Vol.15 / Issue 17
I. Traoré:
An Outline of PVS Semantics for UML Statecharts
/jucs_6_11/an_outline_of_pvs
page 1088 - 1108
Vol.6 / Issue 11
H. Treseler, O. Stursberg, P. W. H. Chung, S. Yang:
An Open Software Architecture for the Verification of Industrial Controllers
/jucs_7_1/an_open_software_architecture
page 37 - 53
Vol.7 / Issue 1
J. Woodcock, R. Banach:
The Verification Grand Challenge
/jucs_13_5/the_verification_grand_challenge
page 661 - 668
Vol.13 / Issue 5
W. Zimmermann, T. Gaul:
On the Construction of Correct Compiler Back-Ends: An ASM-Approach
/jucs_3_5/correct_compiler
page 504 - 567
Vol.3 / Issue 5
L. Zuck, A. Pnueli, Y. Fang, B. Goldberg:
VOC: A Methodology for the Translation Validation of OptimizingCompilers
/jucs_9_3/voc_a_methodology_for
page 223 - 247
Vol.9 / Issue 3
R. Maiani de Mello, E. Nogueira Teixeira, M. Schots, C.M. Lima Werner, G. Horta Travassos:
Verification of Software Product Line Artefacts: A Checklist to Support Feature Model Inspections
/jucs_20_5/verification_of_software_product
page 720 - 745
Vol.20 / Issue 5
F. de Oliveira Jr., R. Lima, M. Cornelio, S. Soares, P. Maciel, R. Barreto, M. Oliveira Jr., E. Tavares:
CML: C Modeling Language
/jucs_13_6/cml_c_modeling_language
page 682 - 700
Vol.13 / Issue 6
J.A. Andrew van der Poll, P. Kotzé, W. Adrian Labuschagne:
Automated Support for Enterprise Information Systems
/jucs_10_11/automated_support_for_enterprise
page 1519 - 1539
Vol.10 / Issue 11