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. 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
	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. 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
	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
	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
	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
	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
	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
	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
	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
	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
	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