@article{MTMT:31360895,
	title = {Automated Generation of Consistent Graph Models with Multiplicity Reasoning},
	url = {https://m2.mtmt.hu/api/publication/31360895},
	author = {Marussy, Kristóf and Semeráth, Oszkár and Varró, Dániel},
	doi = {10.1109/TSE.2020.3025732},
	journal-iso = {IEEE T SOFTWARE ENG},
	journal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING},
	volume = {48},
	unique-id = {31360895},
	issn = {0098-5589},
	abstract = {Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph models is necessitated which is often carried out by solver-based model generation techniques. In many model generation scenarios, one needs more refined control over the generated unit tests to focus on the more relevant models. Type scopes allow to precisely define the required number of newly generated elements, thus one can avoid the generation of unrealistic and highly symmetric models having only a single type of elements. In this paper, we propose a 3-valued scoped partial modeling formalism, which innovatively extends partial graph models with predicate abstraction and counter abstraction. As a result, well-formedness constraints and multiplicity requirements can be evaluated in an approximated way on incomplete (unfinished) models by using advanced graph query engines with numerical solvers (e.g., IP or LP solvers). Based on the refinement of 3-valued scoped partial models, we propose an efficient model generation algorithm that generates models that are both well-formed and satisfy the scope requirements. We show that the proposed approach scales significantly better than existing SAT-solver techniques or the original graph solver without multiplicity reasoning. We illustrate our approach in a complex design-space exploration case study of collaborating satellites introduced by researchers at NASA JPL.},
	year = {2022},
	eissn = {1939-3520},
	pages = {1610-1629},
	orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}
}

@inproceedings{MTMT:32398430,
	title = {Towards Testing ACID Compliance in the LDBC Social Network Benchmark},
	url = {https://m2.mtmt.hu/api/publication/32398430},
	author = {Waudby, Jack and Steer, Benjamin A. and Karimov, Karim and Marton, József and Boncz, Peter and Szárnyas, Gábor},
	booktitle = {Performance Evaluation and Benchmarking},
	doi = {10.1007/978-3-030-84924-5_1},
	unique-id = {32398430},
	abstract = {Verifying ACID compliance is an essential part of database benchmarking, because the integrity of performance results can be undermined as the performance benefits of operating with weaker safety guarantees (at the potential cost of correctness) are well known. Traditionally, benchmarks have specified a number of tests to validate ACID compliance. However, these tests have been formulated in the context of relational database systems and SQL, whereas our scope of benchmarking are systems for graph data, many of which are non-relational. This paper presents a set of data model-agnostic ACID compliance tests for the LDBC (Linked Data Benchmark Council) Social Network Benchmark suite's Interactive (SNB-I) workload, a transaction processing benchmark for graph databases. We test all ACID properties with a particular emphasis on isolation, covering 10 transaction anomalies in total. We present results from implementing the test suite on 5 database systems.},
	keywords = {Computer Science, Software Engineering},
	year = {2021},
	pages = {1-17},
	orcid-numbers = {Marton, József/0000-0003-4752-4234}
}

@inproceedings{MTMT:32098587,
	title = {Incremental whole-program analysis in Datalog with lattices},
	url = {https://m2.mtmt.hu/api/publication/32098587},
	author = {Szabó, Tamás and Erdweg, Sebastian and Bergmann, Gábor},
	booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
	doi = {10.1145/3453483.3454026},
	unique-id = {32098587},
	abstract = {Incremental static analyses provide up-to-date analysis results in time proportional to the size of a code change, not the entire code base. This promises fast feedback to programmers in IDEs and when checking in commits. However, existing incremental analysis frameworks fail to deliver on this promise for whole-program lattice-based data-flow analyses. In particular, prior Datalog-based frameworks yield good incremental performance only for intra-procedural analyses.
		
		In this paper, we first present a methodology to empirically test if a computation is amenable to incrementalization. Using this methodology, we find that incremental whole-program analysis may be possible. Second, we present a new incremental Datalog solver called LADDDER to eliminate the shortcomings of prior Datalog-based analysis frameworks. Our Datalog solver uses a non-standard aggregation semantics which allows us to loosen monotonicity requirements on analyses and to improve the performance of lattice aggregators considerably. Our evaluation on real-world Java code confirms that LADDDER provides up-to-date points-to, constant propagation, and interval information in milliseconds.},
	year = {2021},
	pages = {1-15},
	orcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582}
}

@article{MTMT:32028274,
	title = {Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models},
	url = {https://m2.mtmt.hu/api/publication/32028274},
	author = {Semeráth, Oszkár and Aren, A. Babikian and Boqi, Chen and Chuning, Li and Marussy, Kristóf and Szárnyas, Gábor and Varró, Dániel},
	doi = {10.1007/s10270-021-00884-z},
	journal-iso = {SOFTW SYST MODEL},
	journal = {SOFTWARE AND SYSTEMS MODELING},
	volume = {20},
	unique-id = {32028274},
	issn = {1619-1366},
	abstract = {In this paper, we present a novel technique to automatically synthesize consistent, diverse and structurally realistic domain-specific graph models. A graph model is (1) consistent if it is metamodel-compliant and it satisfies the well-formedness constraints of the domain; (2) it is diverse if local neighborhoods of nodes are highly different; and (1) it is structurally realistic if a synthetic graph is at a close distance to a representative real model according to various graph metrics used in network science, databases or software engineering. Our approach grows models by model extension operators using a hill-climbing strategy in a way that (A) ensures that there are no constraint violation in the models (for consistency reasons), while (B) more realistic candidates are selected to minimize a target metric value (wrt. the representative real model). We evaluate the effectiveness of the approach for generating realistic models using multiple metrics for guidance heuristics and compared to other model generators in the context of three case studies with a large set of real human models. We also highlight that our technique is able to generate a diverse set of models, which is a requirement in many testing scenarios.},
	year = {2021},
	eissn = {1619-1374},
	pages = {1713-1734},
	orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}
}

@article{MTMT:31965063,
	title = {Controllable and decomposable multidirectional synchronizations},
	url = {https://m2.mtmt.hu/api/publication/31965063},
	author = {Bergmann, Gábor},
	doi = {10.1007/s10270-021-00879-w},
	journal-iso = {SOFTW SYST MODEL},
	journal = {SOFTWARE AND SYSTEMS MODELING},
	volume = {20},
	unique-id = {31965063},
	issn = {1619-1366},
	year = {2021},
	eissn = {1619-1374},
	pages = {1735-1774},
	orcid-numbers = {Bergmann, Gábor/0000-0002-2556-2582}
}

@inproceedings{MTMT:31861479,
	title = {A GraphBLAS solution to the SIGMOD 2014 Programming Contest using multi-source BFS},
	url = {https://m2.mtmt.hu/api/publication/31861479},
	author = {Elekes, Márton and Nagy, Attila and Sándor, Dávid and Antal, János Benjamin and Davis, Timothy A. and Szárnyas, Gábor},
	booktitle = {2020 IEEE High Performance Extreme Computing Conference (HPEC)},
	doi = {10.1109/HPEC43674.2020.9286186},
	unique-id = {31861479},
	year = {2020},
	pages = {1-7},
	orcid-numbers = {Elekes, Márton/0000-0002-3558-147X}
}

@article{MTMT:31374125,
	title = {Simulation-based Safety Assessment of High-level Reliability Models},
	url = {https://m2.mtmt.hu/api/publication/31374125},
	author = {Nagy, Simon József and Graics, Bence and Marussy, Kristóf and Vörös, András},
	doi = {10.4204/EPTCS.316.9},
	journal-iso = {ELECTRON PROC THEOR COMPUT SCI},
	journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE},
	volume = {316},
	unique-id = {31374125},
	abstract = {Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our approach builds on engineering models in safety analysis by exploiting the simulation capabilities of recent probabilistic programming and simulation advancements. Thus, it could be applied in accordance with standards and best practices for the analysis of a critical automotive system as part of an industrial collaboration, while leveraging high-level block diagrams and statechart models created by engineers. We demonstrate the applicability of our approach in a case study adapted from the automotive system from the collaboration},
	year = {2020},
	eissn = {2075-2180},
	pages = {240-260},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Marussy, Kristóf/0000-0002-9135-8256}
}

@article{MTMT:31361799,
	title = {A specification language for consistent model generation based on partial models},
	url = {https://m2.mtmt.hu/api/publication/31361799},
	author = {Marussy, Kristóf and Semeráth, Oszkár and Aren, A. Babikian and Varró, Dániel},
	doi = {10.5381/jot.2020.19.3.a12},
	journal-iso = {J OBJECT TECHNOL},
	journal = {JOURNAL OF OBJECT TECHNOLOGY},
	volume = {19},
	unique-id = {31361799},
	issn = {1660-1769},
	year = {2020},
	pages = {1-22},
	orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X}
}

@inproceedings{MTMT:31344297,
	title = {Supporting Dynamic Graphs and Temporal Entity Deletions in the LDBC Social Network Benchmark's Data Generator},
	url = {https://m2.mtmt.hu/api/publication/31344297},
	author = {Waudby, Jack and Steer, Benjamin A. and Prat-Pérez, Arnau and Szárnyas, Gábor},
	booktitle = {Proceedings of the 3rd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA)},
	doi = {10.1145/3398682.3399165},
	unique-id = {31344297},
	year = {2020},
	pages = {1-8}
}

@article{MTMT:31343505,
	title = {Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems},
	url = {https://m2.mtmt.hu/api/publication/31343505},
	author = {Graics, Bence and Molnár, Vince and Vörös, András and Majzik, István and Varró, Dániel},
	doi = {10.1007/s10270-020-00806-5},
	journal-iso = {SOFTW SYST MODEL},
	journal = {SOFTWARE AND SYSTEMS MODELING},
	volume = {19},
	unique-id = {31343505},
	issn = {1619-1366},
	abstract = {The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.},
	keywords = {Formal Semantics; formal verification; Component-based design; composition language; statecharts},
	year = {2020},
	eissn = {1619-1374},
	pages = {1483-1517},
	orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Molnár, Vince/0000-0002-8204-7595; Varró, Dániel/0000-0002-8790-252X}
}